let p1, p2, p, pc be Point of (TOP-REAL 2); for a, b, r being Real st p1 in circle (a,b,r) & p2 in circle (a,b,r) & p in circle (a,b,r) & pc = |[a,b]| & p1 <> p & p2 <> p & not 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) holds
2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2)
let a, b, r be Real; ( p1 in circle (a,b,r) & p2 in circle (a,b,r) & p in circle (a,b,r) & pc = |[a,b]| & p1 <> p & p2 <> p & not 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) implies 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )
assume A1:
p1 in circle (a,b,r)
; ( not p2 in circle (a,b,r) or not p in circle (a,b,r) or not pc = |[a,b]| or not p1 <> p or not p2 <> p or 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )
assume A2:
p2 in circle (a,b,r)
; ( not p in circle (a,b,r) or not pc = |[a,b]| or not p1 <> p or not p2 <> p or 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )
assume A3:
p in circle (a,b,r)
; ( not pc = |[a,b]| or not p1 <> p or not p2 <> p or 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )
assume A4:
pc = |[a,b]|
; ( not p1 <> p or not p2 <> p or 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )
assume that
A5:
p1 <> p
and
A6:
p2 <> p
; ( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )
per cases
( r = 0 or r <> 0 )
;
suppose A7:
r = 0
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )then
|.(p1 - pc).| = 0
by A1, A4, TOPREAL9:43;
then A8:
p1 = pc
by Lm1;
A9:
|.(p2 - pc).| = 0
by A2, A4, A7, TOPREAL9:43;
then
p2 = pc
by Lm1;
then 2
* (angle (p1,p,p2)) =
2
* 0
by A8, COMPLEX2:79
.=
angle (
pc,
pc,
pc)
by COMPLEX2:79
;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by A9, A8, Lm1;
verum end; suppose A10:
r <> 0
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )A11:
|.(p2 - pc).| = r
by A2, A4, TOPREAL9:43;
|.(p1 - pc).| >= 0
;
then
r > 0
by A1, A4, A10, TOPREAL9:43;
then consider p3 being
Point of
(TOP-REAL 2) such that
p <> p3
and A12:
p3 in circle (
a,
b,
r)
and A13:
|[a,b]| in LSeg (
p,
p3)
by A3, Th32;
per cases
( p2 = p3 or p2 <> p3 )
;
suppose
p2 = p3
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by A1, A3, A4, A5, A12, A13, Th31;
verum end; suppose A14:
p2 <> p3
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )A15:
angle (
p2,
pc,
p3)
<> 0
( 2
* (angle (p2,p,p3)) = angle (
p2,
pc,
p3) or 2
* ((angle (p2,p,p3)) - PI) = angle (
p2,
pc,
p3) )
by A2, A3, A4, A6, A12, A13, Th31;
then A20:
angle (
p2,
p,
p3)
<> 0
by A15, COMPLEX2:70;
A21:
( 2
* ((angle (p2,p,p3)) - PI) = angle (
p2,
pc,
p3) implies 2
* (angle (p3,p,p2)) = angle (
p3,
pc,
p2) )
proof
assume A22:
2
* ((angle (p2,p,p3)) - PI) = angle (
p2,
pc,
p3)
;
2 * (angle (p3,p,p2)) = angle (p3,pc,p2)
thus 2
* (angle (p3,p,p2)) =
2
* ((2 * PI) - (angle (p2,p,p3)))
by A20, EUCLID_3:37
.=
(2 * PI) - (2 * ((angle (p2,p,p3)) - PI))
.=
angle (
p3,
pc,
p2)
by A15, A22, EUCLID_3:37
;
verum
end; A23:
angle (
p3,
p,
p2)
= (2 * PI) - (angle (p2,p,p3))
by A20, EUCLID_3:37;
A24:
( 2
* (angle (p2,p,p3)) = angle (
p2,
pc,
p3) implies 2
* ((angle (p3,p,p2)) - PI) = angle (
p3,
pc,
p2) )
proof
assume
2
* (angle (p2,p,p3)) = angle (
p2,
pc,
p3)
;
2 * ((angle (p3,p,p2)) - PI) = angle (p3,pc,p2)
hence 2
* ((angle (p3,p,p2)) - PI) =
(2 * PI) - (angle (p2,pc,p3))
by A23
.=
angle (
p3,
pc,
p2)
by A15, EUCLID_3:37
;
verum
end; A25:
(
angle (
p1,
p,
p2)
= (angle (p1,p,p3)) + (angle (p3,p,p2)) or
(angle (p1,p,p2)) + (2 * PI) = (angle (p1,p,p3)) + (angle (p3,p,p2)) )
by Th4;
per cases
( angle (p1,pc,p2) = (angle (p1,pc,p3)) + (angle (p3,pc,p2)) or (angle (p1,pc,p2)) + (2 * PI) = (angle (p1,pc,p3)) + (angle (p3,pc,p2)) )
by Th4;
suppose A26:
angle (
p1,
pc,
p2)
= (angle (p1,pc,p3)) + (angle (p3,pc,p2))
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )per cases
( ( 2 * (angle (p1,p,p3)) = angle (p1,pc,p3) & 2 * ((angle (p3,p,p2)) - PI) = angle (p3,pc,p2) ) or ( 2 * (angle (p1,p,p3)) = angle (p1,pc,p3) & 2 * (angle (p3,p,p2)) = angle (p3,pc,p2) ) or ( 2 * ((angle (p1,p,p3)) - PI) = angle (p1,pc,p3) & 2 * ((angle (p3,p,p2)) - PI) = angle (p3,pc,p2) ) or ( 2 * ((angle (p1,p,p3)) - PI) = angle (p1,pc,p3) & 2 * (angle (p3,p,p2)) = angle (p3,pc,p2) ) )
by A1, A2, A3, A4, A5, A6, A12, A13, A24, A21, Th31;
suppose
( 2
* (angle (p1,p,p3)) = angle (
p1,
pc,
p3) & 2
* ((angle (p3,p,p2)) - PI) = angle (
p3,
pc,
p2) )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )then
(
angle (
p1,
pc,
p2)
= (2 * (angle (p1,p,p2))) - (2 * PI) or
angle (
p1,
pc,
p2)
= (2 * (angle (p1,p,p2))) + (2 * PI) )
by A25, A26;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by Lm3;
verum end; suppose
( 2
* (angle (p1,p,p3)) = angle (
p1,
pc,
p3) & 2
* (angle (p3,p,p2)) = angle (
p3,
pc,
p2) )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )then
(
angle (
p1,
pc,
p2)
= 2
* (angle (p1,p,p2)) or
angle (
p1,
pc,
p2)
= (2 * (angle (p1,p,p2))) + (4 * PI) )
by A25, A26;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by Lm4;
verum end; suppose
( 2
* ((angle (p1,p,p3)) - PI) = angle (
p1,
pc,
p3) & 2
* ((angle (p3,p,p2)) - PI) = angle (
p3,
pc,
p2) )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )then
angle (
p1,
pc,
p2)
= (2 * ((angle (p1,p,p3)) + (angle (p3,p,p2)))) - (4 * PI)
by A26;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by A25, Lm5;
verum end; suppose
( 2
* ((angle (p1,p,p3)) - PI) = angle (
p1,
pc,
p3) & 2
* (angle (p3,p,p2)) = angle (
p3,
pc,
p2) )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )then
(
angle (
p1,
pc,
p2)
= (2 * (angle (p1,p,p2))) - (2 * PI) or
angle (
p1,
pc,
p2)
= (2 * (angle (p1,p,p2))) + (2 * PI) )
by A25, A26;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by Lm3;
verum end; end; end; suppose A27:
(angle (p1,pc,p2)) + (2 * PI) = (angle (p1,pc,p3)) + (angle (p3,pc,p2))
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )per cases
( ( 2 * (angle (p1,p,p3)) = angle (p1,pc,p3) & 2 * ((angle (p3,p,p2)) - PI) = angle (p3,pc,p2) ) or ( 2 * (angle (p1,p,p3)) = angle (p1,pc,p3) & 2 * (angle (p3,p,p2)) = angle (p3,pc,p2) ) or ( 2 * ((angle (p1,p,p3)) - PI) = angle (p1,pc,p3) & 2 * ((angle (p3,p,p2)) - PI) = angle (p3,pc,p2) ) or ( 2 * ((angle (p1,p,p3)) - PI) = angle (p1,pc,p3) & 2 * (angle (p3,p,p2)) = angle (p3,pc,p2) ) )
by A1, A2, A3, A4, A5, A6, A12, A13, A24, A21, Th31;
suppose
( 2
* (angle (p1,p,p3)) = angle (
p1,
pc,
p3) & 2
* ((angle (p3,p,p2)) - PI) = angle (
p3,
pc,
p2) )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )then
angle (
p1,
pc,
p2)
= (2 * ((angle (p1,p,p3)) + (angle (p3,p,p2)))) - (4 * PI)
by A27;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by A25, Lm5;
verum end; suppose
( 2
* (angle (p1,p,p3)) = angle (
p1,
pc,
p3) & 2
* (angle (p3,p,p2)) = angle (
p3,
pc,
p2) )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )then
(
angle (
p1,
pc,
p2)
= (2 * (angle (p1,p,p2))) - (2 * PI) or
angle (
p1,
pc,
p2)
= (2 * (angle (p1,p,p2))) + (2 * PI) )
by A25, A27;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by Lm3;
verum end; suppose
( 2
* ((angle (p1,p,p3)) - PI) = angle (
p1,
pc,
p3) & 2
* ((angle (p3,p,p2)) - PI) = angle (
p3,
pc,
p2) )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )then
angle (
p1,
pc,
p2)
= (2 * ((angle (p1,p,p3)) + (angle (p3,p,p2)))) - (6 * PI)
by A27;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by A25, Lm6;
verum end; suppose
( 2
* ((angle (p1,p,p3)) - PI) = angle (
p1,
pc,
p3) & 2
* (angle (p3,p,p2)) = angle (
p3,
pc,
p2) )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )then
angle (
p1,
pc,
p2)
= (2 * ((angle (p1,p,p3)) + (angle (p3,p,p2)))) - (4 * PI)
by A27;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by A25, Lm5;
verum end; end; end; end; end; end; end; end;