let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: for a, b, c being Real st a = |.(p1 - p2).| & b = |.(p3 - p2).| & c = |.(p3 - p1).| holds
c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3))))
let a, b, c be Real; :: thesis: ( a = |.(p1 - p2).| & b = |.(p3 - p2).| & c = |.(p3 - p1).| implies c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3)))) )
assume that
A1: ( a = |.(p1 - p2).| & b = |.(p3 - p2).| ) and
A2: c = |.(p3 - p1).| ; :: thesis: c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3))))

per cases ( p1 = p2 or p1 <> p2 ) ;

suppose A3: p1 = p2 ; :: thesis: c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3))))

then |.(p1 - p2).| = |.(0. (TOP-REAL 2)).| by RLVECT_1:5
.= 0 by EUCLID_2:39 ;
hence c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3)))) by A1, A2, A3; :: thesis: verum

end;

suppose A4: p1 <> p2 ; :: thesis: c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3))))

per cases ( p2 = p3 or p2 <> p3 ) ;

suppose A5: p2 = p3 ; :: thesis: c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3))))

then |.(p3 - p2).| = |.(0. (TOP-REAL 2)).| by RLVECT_1:5
.= 0 by EUCLID_2:39 ;
then ((|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2)) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * (cos (angle (p1,p2,p3)))) = |.(- (p1 - p2)).| ^2 by EUCLID:71
.= |.(p2 - p1).| ^2 by RLVECT_1:33 ;
hence c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3)))) by A1, A2, A5; :: thesis: verum

end;

suppose A6: p2 <> p3 ; :: thesis: c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3))))

set c2 = euc2cpx (p3 - p2);
set c1 = euc2cpx (p1 - p2);

A7: now :: thesis: ( not euc2cpx (p1 - p2) = 0 & not euc2cpx (p3 - p2) = 0 )

assume A8: ( euc2cpx (p1 - p2) = 0 or euc2cpx (p3 - p2) = 0 ) ; :: thesis: contradiction

per cases ( euc2cpx (p1 - p2) = 0 or euc2cpx (p3 - p2) = 0 ) by A8;

suppose euc2cpx (p1 - p2) = 0 ; :: thesis: contradiction

hence contradiction by A4, EUCLID_3:18, RLVECT_1:21; :: thesis: verum

end;

suppose euc2cpx (p3 - p2) = 0 ; :: thesis: contradiction

hence contradiction by A6, EUCLID_3:18, RLVECT_1:21; :: thesis: verum

end;

end;

end;

A9: now :: thesis: not |.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).| = 0

assume A10: |.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).| = 0 ; :: thesis: contradiction

per cases ( |.(euc2cpx (p1 - p2)).| = 0 or |.(euc2cpx (p3 - p2)).| = 0 ) by A10;

suppose |.(euc2cpx (p1 - p2)).| = 0 ; :: thesis: contradiction

hence contradiction by A7, COMPLEX1:45; :: thesis: verum

end;

suppose |.(euc2cpx (p3 - p2)).| = 0 ; :: thesis: contradiction

hence contradiction by A7, COMPLEX1:45; :: thesis: verum

end;

end;

end;

A11: ((a ^2) + (b ^2)) - (c ^2) = ((((|.p1.| ^2) - (2 * |(p2,p1)|)) + (|.p2.| ^2)) + (|.(p3 - p2).| ^2)) - (|.(p3 - p1).| ^2) by A1, A2, EUCLID_2:46
.= ((((|.p1.| ^2) - (2 * |(p2,p1)|)) + (|.p2.| ^2)) + (|.(p3 - p2).| ^2)) - (((|.p3.| ^2) - (2 * |(p1,p3)|)) + (|.p1.| ^2)) by EUCLID_2:46
.= ((((- (2 * |(p2,p1)|)) + (|.p2.| ^2)) + (|.(p3 - p2).| ^2)) - (|.p3.| ^2)) + (2 * |(p1,p3)|)
.= ((((- (2 * |(p2,p1)|)) + (|.p2.| ^2)) + (((|.p3.| ^2) - (2 * |(p2,p3)|)) + (|.p2.| ^2))) - (|.p3.| ^2)) + (2 * |(p1,p3)|) by EUCLID_2:46
.= 2 * ((((- |(p2,p1)|) + (|.p2.| ^2)) - |(p2,p3)|) + |(p1,p3)|) ;
(|.(p1 - p2).| * |.(p3 - p2).|) * (cos (angle (p1,p2,p3))) = (|.(p1 - p2).| * |.(p3 - p2).|) * (cos (angle ((euc2cpx (p1 - p2)),(euc2cpx (p3 - p2))))) by Lm7
.= (|.(euc2cpx (p1 - p2)).| * |.(p3 - p2).|) * (cos (angle ((euc2cpx (p1 - p2)),(euc2cpx (p3 - p2))))) by Lm16
.= (|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|) * (cos (angle ((euc2cpx (p1 - p2)),(euc2cpx (p3 - p2))))) by Lm16
.= (|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|) * ((Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))) / (|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|)) by A7, COMPLEX2:69
.= (Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))) / ((|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|) / (|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|)) by XCMPLX_1:81
.= (Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))) / 1 by A9, XCMPLX_1:60
.= (((p1 `1) - (p2 `1)) * ((p3 `1) - (p2 `1))) + (((p1 `2) - (p2 `2)) * ((p3 `2) - (p2 `2))) by Lm16
.= ((((((p1 `1) * (p3 `1)) + ((p1 `2) * (p3 `2))) - ((p1 `1) * (p2 `1))) - ((p2 `1) * (p3 `1))) + ((p2 `1) * (p2 `1))) + (((- ((p1 `2) * (p2 `2))) - ((p2 `2) * (p3 `2))) + ((p2 `2) * (p2 `2)))
.= (((|(p1,p3)| - ((p1 `1) * (p2 `1))) - ((p2 `1) * (p3 `1))) + ((p2 `1) * (p2 `1))) + (((- ((p1 `2) * (p2 `2))) - ((p2 `2) * (p3 `2))) + ((p2 `2) * (p2 `2))) by EUCLID_3:41
.= (((|(p1,p3)| - (((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2)))) - ((p2 `1) * (p3 `1))) + ((p2 `1) * (p2 `1))) + ((- ((p2 `2) * (p3 `2))) + ((p2 `2) * (p2 `2)))
.= (((|(p1,p3)| - |(p1,p2)|) - ((p2 `1) * (p3 `1))) + ((p2 `1) * (p2 `1))) + ((- ((p2 `2) * (p3 `2))) + ((p2 `2) * (p2 `2))) by EUCLID_3:41
.= (((|(p1,p3)| - |(p1,p2)|) - (((p2 `1) * (p3 `1)) + ((p2 `2) * (p3 `2)))) + ((p2 `1) * (p2 `1))) + ((p2 `2) * (p2 `2))
.= (((|(p1,p3)| - |(p1,p2)|) - |(p2,p3)|) + ((p2 `1) * (p2 `1))) + ((p2 `2) * (p2 `2)) by EUCLID_3:41
.= ((|(p1,p3)| - |(p1,p2)|) - |(p2,p3)|) + (((p2 `1) * (p2 `1)) + ((p2 `2) * (p2 `2)))
.= ((|(p1,p3)| - |(p1,p2)|) - |(p2,p3)|) + |(p2,p2)| by EUCLID_3:41
.= ((|(p1,p3)| - |(p1,p2)|) - |(p2,p3)|) + (|.p2.| ^2) by EUCLID_2:36 ;
hence c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3)))) by A1, A11; :: thesis: verum

end;

end;

end;

end;