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]| & pc in LSeg (p,p2) & p1 <> 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]| & pc in LSeg (p,p2) & p1 <> 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 pc in LSeg (p,p2) or not p1 <> 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 pc in LSeg (p,p2) or not p1 <> 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 pc in LSeg (p,p2) or not p1 <> p or 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )
assume that
A4:
pc = |[a,b]|
and
A5:
pc in LSeg (p,p2)
; ( not p1 <> p or 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )
assume A6:
p1 <> 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) )
|.(p2 - pc).| = r
by A2, A4, TOPREAL9:43;
then A11:
pc <> p2
by A10, Lm1;
A12:
euc2cpx p1 <> euc2cpx p
by A6, EUCLID_3:4;
A13:
|.(p1 - pc).| = r
by A1, A4, TOPREAL9:43;
then
pc <> p1
by A10, Lm1;
then A14:
euc2cpx pc <> euc2cpx p1
by EUCLID_3:4;
A15:
|.(p - pc).| = r
by A3, A4, TOPREAL9:43;
then A16:
pc <> p
by A10, Lm1;
then A17:
angle (
p1,
p,
p2)
= angle (
p1,
p,
pc)
by A5, Th10;
|.(pc - p1).| = |.(p - pc).|
by A13, A15, Lm2;
then A18:
angle (
pc,
p1,
p)
= angle (
p1,
p,
pc)
by A6, Th16;
euc2cpx pc <> euc2cpx p
by A16, EUCLID_3:4;
then A19:
(
((angle (pc,p1,p)) + (angle (p1,p,pc))) + (angle (p,pc,p1)) = PI or
((angle (pc,p1,p)) + (angle (p1,p,pc))) + (angle (p,pc,p1)) = 5
* PI )
by A14, A12, COMPLEX2:88;
per cases
( ( (angle (p,pc,p1)) + (angle (p1,pc,p2)) = PI & (2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = PI ) or ( (angle (p,pc,p1)) + (angle (p1,pc,p2)) = 3 * PI & (2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = PI ) or ( (angle (p,pc,p1)) + (angle (p1,pc,p2)) = PI & (2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = 5 * PI ) or ( (angle (p,pc,p1)) + (angle (p1,pc,p2)) = 3 * PI & (2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = 5 * PI ) )
by A5, A16, A11, A19, A18, A17, Th13;
suppose
(
(angle (p,pc,p1)) + (angle (p1,pc,p2)) = PI &
(2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = PI )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )end; suppose A20:
(
(angle (p,pc,p1)) + (angle (p1,pc,p2)) = 3
* PI &
(2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = PI )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )
(
angle (
p1,
pc,
p2)
< 2
* PI &
angle (
p1,
p,
p2)
>= 0 )
by COMPLEX2:70;
then
(- (2 * (angle (p1,p,p2)))) + (angle (p1,pc,p2)) < 0 + (2 * PI)
by XREAL_1:8;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by A20;
verum end; suppose A21:
(
(angle (p,pc,p1)) + (angle (p1,pc,p2)) = PI &
(2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = 5
* PI )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )
(
angle (
p1,
pc,
p2)
>= 0 &
(angle (p1,p,p2)) * 2
< (2 * PI) * 2 )
by COMPLEX2:70, XREAL_1:68;
then
(2 * (angle (p1,p,p2))) + (- (angle (p1,pc,p2))) < ((2 * PI) * 2) + 0
by XREAL_1:8;
hence
( 2
* (angle (p1,p,p2)) = angle (
p1,
pc,
p2) or 2
* ((angle (p1,p,p2)) - PI) = angle (
p1,
pc,
p2) )
by A21;
verum end; suppose
(
(angle (p,pc,p1)) + (angle (p1,pc,p2)) = 3
* PI &
(2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = 5
* PI )
;
( 2 * (angle (p1,p,p2)) = angle (p1,pc,p2) or 2 * ((angle (p1,p,p2)) - PI) = angle (p1,pc,p2) )end; end; end; end;