let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: for a, b, c being real number 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 number ; :: 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 EUCLID:46
.= 0 by EUCLID_2:61 ;
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 EUCLID:46
.= 0 by EUCLID_2:61 ;
then ((|.(p1 - p2).| ^2 ) + (|.(p3 - p2).| ^2 )) - (((2 * |.(p1 - p2).|) * |.(p3 - p2).|) * (cos (angle p1,p2,p3))) = |.(- (p1 - p2)).| ^2 by EUCLID:75
.= |.(p2 - p1).| ^2 by EUCLID:48 ;
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

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:47, EUCLID_3:22; :: thesis: verum

end;

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

hence contradiction by A6, EUCLID:47, EUCLID_3:22; :: thesis: verum

end;

end;

end;

A9: now

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:131; :: thesis: verum

end;

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

hence contradiction by A7, COMPLEX1:131; :: 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:68
.= ((((|.p1.| ^2 ) - (2 * |(p2,p1)|)) + (|.p2.| ^2 )) + (|.(p3 - p2).| ^2 )) - (((|.p3.| ^2 ) - (2 * |(p1,p3)|)) + (|.p1.| ^2 )) by EUCLID_2:68
.= ((((- (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:68
.= 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:83
.= (Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))) / ((|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|) / (|.(euc2cpx (p1 - p2)).| * |.(euc2cpx (p3 - p2)).|)) by XCMPLX_1:82
.= (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:50
.= (((|(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:50
.= (((|(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:50
.= ((|(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:50
.= ((|(p1,p3)| - |(p1,p2)|) - |(p2,p3)|) + (|.p2.| ^2 ) by EUCLID_2:58 ;
hence c ^2 = ((a ^2 ) + (b ^2 )) - (((2 * a) * b) * (cos (angle p1,p2,p3))) by A1, A11; :: thesis: verum

end;

end;

end;

end;