let p1, p2, p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (p1,p2) & p <> p1 & p <> p2 implies angle (p1,p,p2) = PI )
set c1 = euc2cpx (p1 - p);
set c2 = euc2cpx (p2 - p);
assume p in LSeg (p1,p2) ; :: thesis: ( not p <> p1 or not p <> p2 or angle (p1,p,p2) = PI )
then consider l being Real such that
A1: p = ((1 - l) * p1) + (l * p2) and
A2: 0 <= l and
A3: l <= 1 ;
reconsider l = l as Real ;
A4: p2 - p = p2 - (((1 + (- l)) * p1) + (l * p2)) by A1
.= p2 - (((1 * p1) + ((- l) * p1)) + (l * p2)) by RLVECT_1:def 6
.= p2 + ((- 1) * (((1 * p1) + ((- l) * p1)) + (l * p2)))
.= p2 + (((- 1) * ((1 * p1) + ((- l) * p1))) + ((- 1) * (l * p2))) by RLVECT_1:def 5
.= p2 + (((- 1) * (p1 + ((- l) * p1))) + ((- 1) * (l * p2))) by RLVECT_1:def 8
.= p2 + (((- 1) * (p1 + ((- l) * p1))) + (((- 1) * l) * p2)) by RLVECT_1:def 7
.= p2 + ((((- 1) * p1) + ((- 1) * ((- l) * p1))) + ((- l) * p2)) by RLVECT_1:def 5
.= p2 + ((((- 1) * p1) + (((- 1) * (- l)) * p1)) + ((- l) * p2)) by RLVECT_1:def 7
.= p2 + (((- 1) * p1) + ((l * p1) + ((- l) * p2))) by RLVECT_1:def 3
.= p2 + ((- p1) + ((l * p1) + ((- l) * p2)))
.= ((- p1) + p2) + ((l * p1) + ((- l) * p2)) by RLVECT_1:def 3
.= ((- p1) + p2) + ((l * (- (- p1))) + ((- l) * p2))
.= ((- p1) + p2) + ((l * ((- 1) * (- p1))) + ((- l) * p2))
.= ((- p1) + p2) + (((l * (- 1)) * (- p1)) + ((- l) * p2)) by RLVECT_1:def 7
.= ((- p1) + p2) + ((- l) * ((- p1) + p2)) by RLVECT_1:def 5
.= (1 * ((- p1) + p2)) + ((- l) * ((- p1) + p2)) by RLVECT_1:def 8
.= (1 + (- l)) * ((- p1) + p2) by RLVECT_1:def 6
.= (1 - l) * ((- p1) + p2) ;
assume A5: p <> p1 ; :: thesis: ( not p <> p2 or angle (p1,p,p2) = PI )
A6: l <> 0
proof
assume l = 0 ; :: thesis: contradiction
then p = (1 * p1) + (0. (TOP-REAL 2)) by A1, RLVECT_1:10
.= 1 * p1 by RLVECT_1:4
.= p1 by RLVECT_1:def 8 ;
hence contradiction by A5; :: thesis: verum
end;
assume A7: p <> p2 ; :: thesis: angle (p1,p,p2) = PI
l <> 1
proof
assume l = 1 ; :: thesis: contradiction
then p = (0. (TOP-REAL 2)) + (1 * p2) by A1, RLVECT_1:10
.= 1 * p2 by RLVECT_1:4
.= p2 by RLVECT_1:def 8 ;
hence contradiction by A7; :: thesis: verum
end;
then l < 1 by A3, XXREAL_0:1;
then - 1 < - l by XREAL_1:24;
then A8: (- 1) + 1 < (- l) + 1 by XREAL_1:6;
A9: - (euc2cpx (p2 - p)) <> 0
proof
assume - (euc2cpx (p2 - p)) = 0 ; :: thesis: contradiction
then |.(p2 - p).| = 0 by COMPLEX1:44, EUCLID_3:25;
then p2 - p = 0. (TOP-REAL 2) by EUCLID_2:42;
hence contradiction by A7, RLVECT_1:21; :: thesis: verum
end;
set r = - (l / (1 - l));
A10: p1 - p = p1 - (((1 + (- l)) * p1) + (l * p2)) by A1
.= p1 - (((1 * p1) + ((- l) * p1)) + (l * p2)) by RLVECT_1:def 6
.= p1 + ((- 1) * (((1 * p1) + ((- l) * p1)) + (l * p2)))
.= p1 + (((- 1) * ((1 * p1) + ((- l) * p1))) + ((- 1) * (l * p2))) by RLVECT_1:def 5
.= p1 + (((- 1) * (p1 + ((- l) * p1))) + ((- 1) * (l * p2))) by RLVECT_1:def 8
.= p1 + (((- 1) * (p1 + ((- l) * p1))) + (((- 1) * l) * p2)) by RLVECT_1:def 7
.= p1 + ((((- 1) * p1) + ((- 1) * ((- l) * p1))) + ((- l) * p2)) by RLVECT_1:def 5
.= p1 + ((((- 1) * p1) + (((- 1) * (- l)) * p1)) + ((- l) * p2)) by RLVECT_1:def 7
.= p1 + (((- 1) * p1) + ((l * p1) + ((- l) * p2))) by RLVECT_1:def 3
.= p1 + ((- p1) + ((l * p1) + ((- l) * p2)))
.= (p1 + (- p1)) + ((l * p1) + ((- l) * p2)) by RLVECT_1:def 3
.= (0. (TOP-REAL 2)) + ((l * p1) + ((- l) * p2)) by RLVECT_1:5
.= (l * p1) + ((l * (- 1)) * p2) by RLVECT_1:4
.= (l * p1) + (l * ((- 1) * p2)) by RLVECT_1:def 7
.= (l * p1) + (l * (- p2))
.= l * (p1 - p2) by RLVECT_1:def 5 ;
cpx2euc ((euc2cpx (p2 - p)) * (- (l / (1 - l)))) = (- (l / (1 - l))) * (cpx2euc (euc2cpx (p2 - p))) by EUCLID_3:19
.= (- (l / (1 - l))) * ((1 - l) * ((- p1) + p2)) by A4, EUCLID_3:2
.= ((- (l / (1 - l))) * (1 - l)) * ((- p1) + p2) by RLVECT_1:def 7
.= (((- l) / (1 - l)) * (1 - l)) * ((- p1) + p2) by XCMPLX_1:187
.= (((1 - l) / (1 - l)) * (- l)) * ((- p1) + p2) by XCMPLX_1:75
.= (1 * (- l)) * ((- p1) + p2) by A8, XCMPLX_1:60
.= (l * (- 1)) * ((- p1) + p2)
.= l * ((- 1) * ((- p1) + p2)) by RLVECT_1:def 7
.= l * (((- 1) * (- p1)) + ((- 1) * p2)) by RLVECT_1:def 5
.= l * ((- (- p1)) + ((- 1) * p2))
.= l * ((- (- p1)) + (- p2))
.= l * ((- (- p1)) + (- p2))
.= l * (p1 + (- p2))
.= cpx2euc (euc2cpx (p1 - p)) by A10, EUCLID_3:2 ;
then euc2cpx (p1 - p) = (euc2cpx (p2 - p)) * (- (l / (1 - l))) by EUCLID_3:3;
then A11: Arg (- (euc2cpx (p2 - p))) = Arg (euc2cpx (p1 - p)) by A2, A6, A8, COMPLEX2:28;
angle ((euc2cpx (p1 - p)),(- (euc2cpx (p2 - p)))) = 0
proof
per cases ( (Arg (- (euc2cpx (p2 - p)))) - (Arg (euc2cpx (p1 - p))) < 0 or (Arg (- (euc2cpx (p2 - p)))) - (Arg (euc2cpx (p1 - p))) >= 0 ) ;
suppose (Arg (- (euc2cpx (p2 - p)))) - (Arg (euc2cpx (p1 - p))) < 0 ; :: thesis: angle ((euc2cpx (p1 - p)),(- (euc2cpx (p2 - p)))) = 0
hence angle ((euc2cpx (p1 - p)),(- (euc2cpx (p2 - p)))) = 0 by A11; :: thesis: verum
end;
suppose (Arg (- (euc2cpx (p2 - p)))) - (Arg (euc2cpx (p1 - p))) >= 0 ; :: thesis: angle ((euc2cpx (p1 - p)),(- (euc2cpx (p2 - p)))) = 0
hence angle ((euc2cpx (p1 - p)),(- (euc2cpx (p2 - p)))) = 0 by A11, A9, Lm11; :: thesis: verum
end;
end;
end;
then angle ((euc2cpx (p1 - p)),(- (- (euc2cpx (p2 - p))))) = PI by A9, COMPLEX2:68;
hence angle (p1,p,p2) = PI by Lm7; :: thesis: verum