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]| & 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; :: thesis: ( 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) ; :: thesis: ( 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) ; :: thesis: ( 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) ; :: thesis: ( 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]| ; :: thesis: ( 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 ; :: 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) )
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 ; :: 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) ) by A1, A3, A4, A5, A12, A13, Th31; :: thesis: verum
end;
suppose A14: p2 <> p3 ; :: thesis: ( 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
proof
set z3 = euc2cpx (p3 - pc);
set z2 = euc2cpx (p2 - pc);
assume angle (p2,pc,p3) = 0 ; :: thesis: contradiction
then A16: Arg (p2 - pc) = Arg (p3 - pc) by EUCLID_3:36;
A17: |.(p2 - pc).| = |.(p3 - pc).| by A4, A11, A12, TOPREAL9:43;
A18: |.(euc2cpx (p2 - pc)).| = |.(p2 - pc).| by EUCLID_3:25
.= |.(euc2cpx (p3 - pc)).| by A17, EUCLID_3:25 ;
A19: euc2cpx (p2 - pc) = (|.(euc2cpx (p2 - pc)).| * (cos (Arg (euc2cpx (p2 - pc))))) + ((|.(euc2cpx (p2 - pc)).| * (sin (Arg (euc2cpx (p2 - pc))))) * <i>) by COMPTRIG:62
.= euc2cpx (p3 - pc) by A16, A18, COMPTRIG:62 ;
p2 = p2 + (0. (TOP-REAL 2)) by RLVECT_1:4
.= p2 + (pc + (- pc)) by RLVECT_1:5
.= (p2 + (- pc)) + pc by RLVECT_1:def 3
.= (p3 - pc) + pc by A19, EUCLID_3:4
.= p3 + (pc + (- pc)) by RLVECT_1:def 3
.= p3 + (0. (TOP-REAL 2)) by RLVECT_1:5
.= p3 by RLVECT_1:4 ;
hence contradiction by A14; :: thesis: verum
end;
( 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) ; :: thesis: 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 ; :: thesis: 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) ; :: thesis: 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 ;
:: thesis: 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)) ; :: thesis: ( 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) ) ; :: thesis: ( 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; :: thesis: verum
end;
suppose ( 2 * (angle (p1,p,p3)) = angle (p1,pc,p3) & 2 * (angle (p3,p,p2)) = angle (p3,pc,p2) ) ; :: thesis: ( 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; :: thesis: verum
end;
suppose ( 2 * ((angle (p1,p,p3)) - PI) = angle (p1,pc,p3) & 2 * ((angle (p3,p,p2)) - PI) = angle (p3,pc,p2) ) ; :: thesis: ( 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; :: thesis: verum
end;
suppose ( 2 * ((angle (p1,p,p3)) - PI) = angle (p1,pc,p3) & 2 * (angle (p3,p,p2)) = angle (p3,pc,p2) ) ; :: thesis: ( 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; :: thesis: verum
end;
end;
end;
suppose A27: (angle (p1,pc,p2)) + (2 * PI) = (angle (p1,pc,p3)) + (angle (p3,pc,p2)) ; :: thesis: ( 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) ) ; :: thesis: ( 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; :: thesis: verum
end;
suppose ( 2 * (angle (p1,p,p3)) = angle (p1,pc,p3) & 2 * (angle (p3,p,p2)) = angle (p3,pc,p2) ) ; :: thesis: ( 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; :: thesis: verum
end;
suppose ( 2 * ((angle (p1,p,p3)) - PI) = angle (p1,pc,p3) & 2 * ((angle (p3,p,p2)) - PI) = angle (p3,pc,p2) ) ; :: thesis: ( 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; :: thesis: verum
end;
suppose ( 2 * ((angle (p1,p,p3)) - PI) = angle (p1,pc,p3) & 2 * (angle (p3,p,p2)) = angle (p3,pc,p2) ) ; :: thesis: ( 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; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;