let p1, p2, p3, p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (p2,p3) & p <> p2 implies angle (p3,p2,p1) = angle (p,p2,p1) )
set c = euc2cpx (p - p2);
set c1 = euc2cpx (p1 - p2);
set c3 = euc2cpx (p3 - p2);
assume p in LSeg (p2,p3) ; :: thesis: ( not p <> p2 or angle (p3,p2,p1) = angle (p,p2,p1) )
then consider l being Real such that
A1: p = ((1 - l) * p2) + (l * p3) and
A2: 0 <= l and
l <= 1 ;
reconsider l = l as Real ;
A3: p - p2 = (((1 + (- l)) * p2) + (l * p3)) - p2 by A1
.= (((1 * p2) + ((- l) * p2)) + (l * p3)) - p2 by RLVECT_1:def 6
.= ((p2 + ((- l) * p2)) + (l * p3)) - p2 by RLVECT_1:def 8
.= (p2 + ((- l) * p2)) + ((l * p3) + (- p2)) by RLVECT_1:def 3
.= p2 + (((- l) * p2) + ((l * p3) + (- p2))) by RLVECT_1:def 3
.= p2 + ((- p2) + (((- l) * p2) + (l * p3))) by RLVECT_1:def 3
.= (p2 + (- p2)) + (((- l) * p2) + (l * p3)) by RLVECT_1:def 3
.= (0. (TOP-REAL 2)) + (((- l) * p2) + (l * p3)) by RLVECT_1:5
.= ((l * (- 1)) * p2) + (l * p3) by RLVECT_1:4
.= (l * ((- 1) * p2)) + (l * p3) by RLVECT_1:def 7
.= (l * (- p2)) + (l * p3)
.= l * (p3 - p2) by RLVECT_1:def 5 ;
assume A4: p <> p2 ; :: thesis: angle (p3,p2,p1) = angle (p,p2,p1)
A5: l <> 0 cpx2euc ((euc2cpx (p3 - p2)) * l) = l * (cpx2euc (euc2cpx (p3 - p2))) by EUCLID_3:19
.= l * (p3 - p2) by EUCLID_3:2
.= cpx2euc (euc2cpx (p - p2)) by A3, EUCLID_3:2 ;
then euc2cpx (p - p2) = (euc2cpx (p3 - p2)) * l by EUCLID_3:3;
then A6: Arg (euc2cpx (p - p2)) = Arg (euc2cpx (p3 - p2)) by A2, A5, COMPLEX2:27;
angle ((euc2cpx (p3 - p2)),(euc2cpx (p1 - p2))) = angle ((euc2cpx (p - p2)),(euc2cpx (p1 - p2))) hence angle (p3,p2,p1) = angle ((euc2cpx (p - p2)),(euc2cpx (p1 - p2))) by Lm7
.= angle (p,p2,p1) by Lm7 ;
:: thesis: verum