let p1, p2, p3, p be Point of (TOP-REAL 2); :: thesis: ( |.(p1 - p3).| = |.(p2 - p3).| & p in LSeg (p1,p2) & p <> p3 & p <> p1 & ( angle (p3,p,p1) = PI / 2 or angle (p3,p,p1) = (3 / 2) * PI ) implies angle (p1,p3,p) = angle (p,p3,p2) )
assume A1: |.(p1 - p3).| = |.(p2 - p3).| ; :: thesis: ( not p in LSeg (p1,p2) or not p <> p3 or not p <> p1 or ( not angle (p3,p,p1) = PI / 2 & not angle (p3,p,p1) = (3 / 2) * PI ) or angle (p1,p3,p) = angle (p,p3,p2) )
then A2: |.(p3 - p1).| = |.(p2 - p3).| by Lm2;
assume A3: p in LSeg (p1,p2) ; :: thesis: ( not p <> p3 or not p <> p1 or ( not angle (p3,p,p1) = PI / 2 & not angle (p3,p,p1) = (3 / 2) * PI ) or angle (p1,p3,p) = angle (p,p3,p2) )
assume that
A4: p <> p3 and
A5: p <> p1 ; :: thesis: ( ( not angle (p3,p,p1) = PI / 2 & not angle (p3,p,p1) = (3 / 2) * PI ) or angle (p1,p3,p) = angle (p,p3,p2) )
assume A6: ( angle (p3,p,p1) = PI / 2 or angle (p3,p,p1) = (3 / 2) * PI ) ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)
per cases ( p1 = p2 or p1 <> p2 ) ;
suppose A7: p1 = p2 ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)
then LSeg (p1,p2) = {p1} by RLTOPSP1:70;
then p = p1 by A3, TARSKI:def 1;
hence angle (p1,p3,p) = angle (p,p3,p2) by A7; :: thesis: verum
end;
suppose A8: p1 <> p2 ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)
per cases ( p <> p2 or p = p2 ) ;
suppose A9: p <> p2 ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)
p2 <> p3
proof
assume A10: p2 = p3 ; :: thesis: contradiction
then |.(p3 - p1).| = 0 by A2, Lm1;
hence contradiction by A8, A10, Lm1; :: thesis: verum
end;
then A11: euc2cpx p2 <> euc2cpx p3 by EUCLID_3:4;
p1 <> p3
proof
assume A12: p1 = p3 ; :: thesis: contradiction
then |.(p2 - p3).| = 0 by A1, Lm1;
hence contradiction by A8, A12, Lm1; :: thesis: verum
end;
then A13: euc2cpx p1 <> euc2cpx p3 by EUCLID_3:4;
A14: ( euc2cpx p <> euc2cpx p1 & euc2cpx p <> euc2cpx p3 ) by A4, A5, EUCLID_3:4;
A15: ( angle (p1,p,p3) = angle (p3,p,p2) & euc2cpx p <> euc2cpx p2 ) by A3, A5, A6, A9, Th14, EUCLID_3:4;
A16: angle (p3,p1,p) = angle (p3,p1,p2) by A3, A5, Th10
.= angle (p1,p2,p3) by A2, A8, Th16
.= angle (p,p2,p3) by A3, A9, Th9 ;
A17: angle (p,p3,p1) = angle (p2,p3,p)
proof
per cases ( ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = PI ) or ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = 5 * PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = 5 * PI ) or ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = 5 * PI ) or ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = 5 * PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = PI ) ) by A16, A14, A13, A11, A15, COMPLEX2:88;
suppose ( ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = PI ) or ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = 5 * PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = 5 * PI ) ) ; :: thesis: angle (p,p3,p1) = angle (p2,p3,p)
hence angle (p,p3,p1) = angle (p2,p3,p) ; :: thesis: verum
end;
suppose A18: ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = 5 * PI ) ; :: thesis: angle (p,p3,p1) = angle (p2,p3,p)
( angle (p2,p3,p) < 2 * PI & angle (p,p3,p1) >= 0 ) by COMPLEX2:70;
then A19: (angle (p2,p3,p)) - (angle (p,p3,p1)) < (2 * PI) - 0 by XREAL_1:14;
(angle (p2,p3,p)) - (angle (p,p3,p1)) = 4 * PI by A18;
hence angle (p,p3,p1) = angle (p2,p3,p) by A19, XREAL_1:64; :: thesis: verum
end;
suppose A20: ( ((angle (p,p2,p3)) + (angle (p,p3,p1))) + (angle (p3,p,p2)) = 5 * PI & ((angle (p,p2,p3)) + (angle (p2,p3,p))) + (angle (p3,p,p2)) = PI ) ; :: thesis: angle (p,p3,p1) = angle (p2,p3,p)
( angle (p,p3,p1) < 2 * PI & angle (p2,p3,p) >= 0 ) by COMPLEX2:70;
then A21: (angle (p,p3,p1)) - (angle (p2,p3,p)) < (2 * PI) - 0 by XREAL_1:14;
(angle (p,p3,p1)) - (angle (p2,p3,p)) = 4 * PI by A20;
hence angle (p,p3,p1) = angle (p2,p3,p) by A21, XREAL_1:64; :: thesis: verum
end;
end;
end;
per cases ( angle (p,p3,p1) = 0 or angle (p,p3,p1) <> 0 ) ;
suppose A22: angle (p,p3,p1) = 0 ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)
then angle (p1,p3,p) = 0 by EUCLID_3:36;
hence angle (p1,p3,p) = angle (p,p3,p2) by A17, A22, EUCLID_3:36; :: thesis: verum
end;
suppose A23: angle (p,p3,p1) <> 0 ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)
then angle (p1,p3,p) = (2 * PI) - (angle (p,p3,p1)) by EUCLID_3:37;
hence angle (p1,p3,p) = angle (p,p3,p2) by A17, A23, EUCLID_3:37; :: thesis: verum
end;
end;
end;
suppose A24: p = p2 ; :: thesis: angle (p1,p3,p) = angle (p,p3,p2)
then |.(p3 - p1).| = |.(p - p3).| by A1, Lm2
.= |.(p3 - p).| by Lm2 ;
then (|.(p3 - p1).| ^2) + (|.(p1 - p).| ^2) = |.(p3 - p1).| ^2 by A4, A5, A6, EUCLID_3:46;
then |.(p1 - p).| = 0 ;
hence angle (p1,p3,p) = angle (p,p3,p2) by A24, Lm1; :: thesis: verum
end;
end;
end;
end;