let p1, p2, p be Point of (TOP-REAL 2); :: thesis: ( angle (p1,p,p2) = PI implies p in LSeg (p1,p2) )
assume A1: angle (p1,p,p2) = PI ; :: thesis: p in LSeg (p1,p2)
set r = |.(p - p1).|;
set b = p1 `2 ;
set a = p1 `1 ;
A2: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53;
per cases ( p = p1 or p = p2 or ( p <> p1 & p <> p2 ) ) ;
suppose ( p = p1 or p = p2 ) ; :: thesis: p in LSeg (p1,p2)
hence p in LSeg (p1,p2) by RLTOPSP1:68; :: thesis: verum
end;
suppose A3: ( p <> p1 & p <> p2 ) ; :: thesis: p in LSeg (p1,p2)
A4: |.(p2 - p1).| ^2 = ((|.(p1 - p).| ^2) + (|.(p2 - p).| ^2)) - (((2 * |.(p1 - p).|) * |.(p2 - p).|) * (- 1)) by A1, Th7, SIN_COS:77
.= (|.(p1 - p).| + |.(p2 - p).|) ^2 ;
|.(p2 - p1).| > |.(p - p1).|
proof
assume |.(p2 - p1).| <= |.(p - p1).| ; :: thesis: contradiction
then |.(p2 - p1).| ^2 <= |.(p - p1).| ^2 by SQUARE_1:15;
then (|.(p - p1).| + |.(p2 - p).|) ^2 <= |.(p - p1).| ^2 by A4, Lm2;
then (((|.(p - p1).| ^2) + ((2 * |.(p - p1).|) * |.(p2 - p).|)) + (|.(p2 - p).| ^2)) - (|.(p - p1).| ^2) <= (|.(p - p1).| ^2) - (|.(p - p1).| ^2) by XREAL_1:9;
then A5: ((2 * |.(p - p1).|) + |.(p2 - p).|) * |.(p2 - p).| <= 0 ;
|.(p2 - p).| <> 0 by A3, Lm1;
hence contradiction by A5; :: thesis: verum
end;
then p2 in { p4 where p4 is Point of (TOP-REAL 2) : |.(p4 - |[(p1 `1),(p1 `2)]|).| > |.(p - p1).| } by A2;
then A6: p2 in outside_of_circle ((p1 `1),(p1 `2),|.(p - p1).|) by JGRAPH_6:def 8;
A7: |.(p1 - |[(p1 `1),(p1 `2)]|).| = 0 by A2, Lm1;
|.(p - p1).| <> 0 by A3, Lm1;
then p1 in { p4 where p4 is Point of (TOP-REAL 2) : |.(p4 - |[(p1 `1),(p1 `2)]|).| < |.(p - p1).| } by A7;
then p1 in inside_of_circle ((p1 `1),(p1 `2),|.(p - p1).|) by JGRAPH_6:def 6;
then consider p3 being Point of (TOP-REAL 2) such that
A8: p3 in (LSeg (p1,p2)) /\ (circle ((p1 `1),(p1 `2),|.(p - p1).|)) by A6, Lm17;
A9: euc2cpx p1 <> euc2cpx p2 by A1, COMPLEX2:79;
A10: ( euc2cpx p <> euc2cpx p1 & euc2cpx p <> euc2cpx p2 ) by A3, EUCLID_3:4;
A11: angle (p,p1,p2) = 0
proof
assume angle (p,p1,p2) <> 0 ; :: thesis: contradiction
then A12: angle (p,p1,p2) > 0 by COMPLEX2:70;
A13: angle (p,p1,p2) < 2 * PI by COMPLEX2:70;
per cases ( ((angle (p,p1,p2)) + (angle (p1,p2,p))) + (angle (p2,p,p1)) = PI or ((angle (p,p1,p2)) + (angle (p1,p2,p))) + (angle (p2,p,p1)) = 5 * PI ) by A10, A9, COMPLEX2:88;
suppose A14: ((angle (p,p1,p2)) + (angle (p1,p2,p))) + (angle (p2,p,p1)) = PI ; :: thesis: contradiction
A15: angle (p1,p2,p) >= 0 by COMPLEX2:70;
((angle (p,p1,p2)) + (angle (p1,p2,p))) + PI = PI by A1, A14, COMPLEX2:82;
hence contradiction by A12, A15; :: thesis: verum
end;
suppose A16: ((angle (p,p1,p2)) + (angle (p1,p2,p))) + (angle (p2,p,p1)) = 5 * PI ; :: thesis: contradiction
angle (p1,p2,p) < 2 * PI by COMPLEX2:70;
then A17: (angle (p,p1,p2)) + (angle (p1,p2,p)) < (2 * PI) + (2 * PI) by A13, XREAL_1:8;
((angle (p,p1,p2)) + (angle (p1,p2,p))) + PI = 5 * PI by A1, A16, COMPLEX2:82;
hence contradiction by A17; :: thesis: verum
end;
end;
end;
p3 in circle ((p1 `1),(p1 `2),|.(p - p1).|) by A8, XBOOLE_0:def 4;
then p3 in { p4 where p4 is Point of (TOP-REAL 2) : |.(p4 - |[(p1 `1),(p1 `2)]|).| = |.(p - p1).| } by JGRAPH_6:def 5;
then A18: ex p4 being Point of (TOP-REAL 2) st
( p3 = p4 & |.(p4 - |[(p1 `1),(p1 `2)]|).| = |.(p - p1).| ) ;
then A19: |.(p3 - p1).| = |.(p - p1).| by EUCLID:53;
|.(p - p1).| <> 0 by A3, Lm1;
then A20: p3 <> p1 by A2, A18, Lm1;
A21: p3 in LSeg (p1,p2) by A8, XBOOLE_0:def 4;
|.(p3 - p).| ^2 = ((|.(p - p1).| ^2) + (|.(p3 - p1).| ^2)) - (((2 * |.(p - p1).|) * |.(p3 - p1).|) * (cos (angle (p,p1,p3)))) by Th7
.= ((|.(p - p1).| ^2) + (|.(p - p1).| ^2)) - (((2 * |.(p - p1).|) * |.(p - p1).|) * (cos 0)) by A21, A19, A20, A11, Th10
.= 0 by SIN_COS:31 ;
then |.(p3 - p).| = 0 ;
hence p in LSeg (p1,p2) by A21, Lm1; :: thesis: verum
end;
end;