let p1, p3, p2, 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:71;
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:6;
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:6;
A14: ( euc2cpx p <> euc2cpx p1 & euc2cpx p <> euc2cpx p3 ) by A4, A5, EUCLID_3:6;
A15: ( angle p1,p,p3 = angle p3,p,p2 & euc2cpx p <> euc2cpx p2 ) by A3, A5, A6, A9, Th14, EUCLID_3:6;
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:102;
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:84;
then A19: (angle p2,p3,p) - (angle p,p3,p1) < (2 * PI ) - 0 by XREAL_1:16;
(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:66; :: 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:84;
then A21: (angle p,p3,p1) - (angle p2,p3,p) < (2 * PI ) - 0 by XREAL_1:16;
(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:66; :: 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:45;
hence angle p1,p3,p = angle p,p3,p2 by A17, A22, EUCLID_3:45; :: 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:46;
hence angle p1,p3,p = angle p,p3,p2 by A17, A23, EUCLID_3:46; :: 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:55;
then |.(p1 - p).| = 0 ;
hence angle p1,p3,p = angle p,p3,p2 by A24, Lm1; :: thesis: verum
end;
end;
end;
end;