let p1, p2, p, pc be Point of (TOP-REAL 2); :: thesis: 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; :: thesis: ( 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) ; :: thesis: ( 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) ; :: thesis: ( 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) ; :: thesis: ( 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) ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum
end;
suppose A10: r <> 0 ; :: thesis: ( 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 ) ; :: thesis: ( 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) ) ; :: thesis: verum
end;
suppose A20: ( (angle (p,pc,p1)) + (angle (p1,pc,p2)) = 3 * PI & (2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = PI ) ; :: thesis: ( 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; :: thesis: verum
end;
suppose A21: ( (angle (p,pc,p1)) + (angle (p1,pc,p2)) = PI & (2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = 5 * PI ) ; :: thesis: ( 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; :: thesis: verum
end;
suppose ( (angle (p,pc,p1)) + (angle (p1,pc,p2)) = 3 * PI & (2 * (angle (p1,p,p2))) + (angle (p,pc,p1)) = 5 * PI ) ; :: thesis: ( 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) ) ; :: thesis: verum
end;
end;
end;
end;