let p1, p2, p3, p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (p1,p2) & not p3 in LSeg (p1,p2) & angle (p1,p3,p2) > PI & p <> p2 implies angle (p,p3,p2) >= angle (p1,p3,p2) )
assume A1: p in LSeg (p1,p2) ; :: thesis: ( p3 in LSeg (p1,p2) or not angle (p1,p3,p2) > PI or not p <> p2 or angle (p,p3,p2) >= angle (p1,p3,p2) )
assume A2: not p3 in LSeg (p1,p2) ; :: thesis: ( not angle (p1,p3,p2) > PI or not p <> p2 or angle (p,p3,p2) >= angle (p1,p3,p2) )
assume A3: angle (p1,p3,p2) > PI ; :: thesis: ( not p <> p2 or angle (p,p3,p2) >= angle (p1,p3,p2) )
assume A4: p <> p2 ; :: thesis: angle (p,p3,p2) >= angle (p1,p3,p2)
assume A5: angle (p,p3,p2) < angle (p1,p3,p2) ; :: thesis: contradiction
per cases ( p = p1 or p1 = p2 or ( p1 <> p2 & p <> p1 ) ) ;
suppose p = p1 ; :: thesis: contradiction
hence contradiction by A5; :: thesis: verum
end;
suppose A6: p1 = p2 ; :: thesis: contradiction
then p in {p2} by A1, RLTOPSP1:70;
hence contradiction by A5, A6, TARSKI:def 1; :: thesis: verum
end;
suppose A7: ( p1 <> p2 & p <> p1 ) ; :: thesis: contradiction
then A8: euc2cpx p2 <> euc2cpx p1 by EUCLID_3:4;
A9: euc2cpx p <> euc2cpx p2 by A4, EUCLID_3:4;
A10: angle (p3,p2,p1) = angle (p3,p2,p) by A1, A4, Th10;
A11: euc2cpx p <> euc2cpx p1 by A7, EUCLID_3:4;
A12: euc2cpx p <> euc2cpx p3 by A1, A2, EUCLID_3:4;
A13: p3 <> p1 by A2, RLTOPSP1:68;
then A14: euc2cpx p3 <> euc2cpx p1 by EUCLID_3:4;
A15: p3 <> p2 by A2, RLTOPSP1:68;
then A16: euc2cpx p3 <> euc2cpx p2 by EUCLID_3:4;
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
proof
per cases ( ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI ) or ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5 * PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5 * PI ) or ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5 * PI ) or ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5 * PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI ) ) by A16, A14, A8, A12, A9, COMPLEX2:88;
suppose ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI ) ; :: thesis: (angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
hence (angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3)) by A10; :: thesis: verum
end;
suppose ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5 * PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5 * PI ) ; :: thesis: (angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
hence (angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3)) by A10; :: thesis: verum
end;
suppose A17: ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5 * PI ) ; :: thesis: (angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
A18: ( angle (p1,p3,p2) >= 0 & angle (p2,p1,p3) >= 0 ) by COMPLEX2:70;
angle (p2,p,p3) < 2 * PI by COMPLEX2:70;
then A19: - (angle (p2,p,p3)) > - (2 * PI) by XREAL_1:24;
angle (p,p3,p2) < 2 * PI by COMPLEX2:70;
then - (angle (p,p3,p2)) > - (2 * PI) by XREAL_1:24;
then (- (angle (p,p3,p2))) + (- (angle (p2,p,p3))) > (- (2 * PI)) + (- (2 * PI)) by A19, XREAL_1:8;
then ((angle (p1,p3,p2)) + (angle (p2,p1,p3))) + ((- (angle (p,p3,p2))) - (angle (p2,p,p3))) > (0 + 0) + ((- (2 * PI)) - (2 * PI)) by A18, XREAL_1:8;
hence (angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3)) by A10, A17; :: thesis: verum
end;
suppose A20: ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5 * PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI ) ; :: thesis: (angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
( angle (p2,p1,p3) < 2 * PI & angle (p1,p3,p2) < 2 * PI ) by COMPLEX2:70;
then A21: (angle (p2,p1,p3)) + (angle (p1,p3,p2)) < (2 * PI) + (2 * PI) by XREAL_1:8;
( angle (p,p3,p2) >= 0 & angle (p2,p,p3) >= 0 ) by COMPLEX2:70;
then ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + ((- (angle (p,p3,p2))) - (angle (p2,p,p3))) < ((2 * PI) + (2 * PI)) + (0 + 0) by A21, XREAL_1:8;
hence (angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3)) by A10, A20; :: thesis: verum
end;
end;
end;
then angle (p2,p1,p3) < angle (p2,p,p3) by A5, XREAL_1:8;
then A22: angle (p,p1,p3) < angle (p2,p,p3) by A1, Th9;
per cases ( ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI ) or ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = 3 * PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI ) or ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5 * PI ) or ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = 3 * PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5 * PI ) ) by A1, A4, A14, A12, A11, Th13, COMPLEX2:88;
suppose A23: ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI ) ; :: thesis: contradiction
p1,p3,p2 are_mutually_distinct by A7, A13, A15, ZFMISC_1:def 5;
then angle (p2,p1,p3) > PI by A3, Th24;
then A24: angle (p,p1,p3) > PI by A1, A7, Th9;
p,p1,p3 are_mutually_distinct by A1, A2, A7, A13, ZFMISC_1:def 5;
then ( angle (p1,p3,p) > PI & angle (p3,p,p1) > PI ) by A24, Th24;
then (angle (p3,p,p1)) + (angle (p1,p3,p)) > PI + PI by XREAL_1:8;
then A25: ((angle (p3,p,p1)) + (angle (p1,p3,p))) + (angle (p,p1,p3)) > (2 * PI) + PI by A24, XREAL_1:8;
1 * PI < 3 * PI by XREAL_1:68;
hence contradiction by A23, A25; :: thesis: verum
end;
suppose A26: ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = 3 * PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI ) ; :: thesis: contradiction
A27: ( angle (p,p1,p3) >= 0 & angle (p1,p3,p) >= 0 ) by COMPLEX2:70;
angle (p2,p,p3) = ((angle (p,p1,p3)) + (angle (p1,p3,p))) + (2 * PI) by A26;
then angle (p2,p,p3) >= 0 + (2 * PI) by A27, XREAL_1:6;
hence contradiction by COMPLEX2:70; :: thesis: verum
end;
suppose A28: ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5 * PI ) ; :: thesis: contradiction
( angle (p,p1,p3) < 2 * PI & angle (p1,p3,p) < 2 * PI ) by COMPLEX2:70;
then (angle (p,p1,p3)) + (angle (p1,p3,p)) < (2 * PI) + (2 * PI) by XREAL_1:8;
then (angle (p2,p,p3)) + (4 * PI) < 0 + (4 * PI) by A28;
then angle (p2,p,p3) < 0 by XREAL_1:6;
hence contradiction by COMPLEX2:70; :: thesis: verum
end;
suppose ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = 3 * PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5 * PI ) ; :: thesis: contradiction
then (angle (p2,p,p3)) + (2 * PI) = (angle (p,p1,p3)) + (angle (p1,p3,p)) ;
then (angle (p2,p,p3)) + (2 * PI) < (angle (p2,p,p3)) + (angle (p1,p3,p)) by A22, XREAL_1:6;
then 2 * PI < angle (p1,p3,p) by XREAL_1:6;
hence contradiction by COMPLEX2:70; :: thesis: verum
end;
end;
end;
end;