let p1, p2, p3, p4, p5, p6 be Point of (TOP-REAL 2); :: thesis: ( p3 <> p2 & p3 <> p1 & p2 <> p1 & p5 <> p6 & p5 <> p4 & p6 <> p4 & angle (p1,p2,p3) <> PI & angle (p2,p3,p1) <> PI & angle (p3,p1,p2) <> PI & angle (p4,p5,p6) <> PI & angle (p5,p6,p4) <> PI & angle (p6,p4,p5) <> PI & angle (p1,p2,p3) = angle (p4,p5,p6) & angle (p3,p1,p2) = angle (p6,p4,p5) implies |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| )
assume that
A1: ( p3 <> p2 & p3 <> p1 ) and
A2: p2 <> p1 ; :: thesis: ( not p5 <> p6 or not p5 <> p4 or not p6 <> p4 or not angle (p1,p2,p3) <> PI or not angle (p2,p3,p1) <> PI or not angle (p3,p1,p2) <> PI or not angle (p4,p5,p6) <> PI or not angle (p5,p6,p4) <> PI or not angle (p6,p4,p5) <> PI or not angle (p1,p2,p3) = angle (p4,p5,p6) or not angle (p3,p1,p2) = angle (p6,p4,p5) or |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| )
A3: ( euc2cpx p3 <> euc2cpx p2 & euc2cpx p3 <> euc2cpx p1 ) by A1, EUCLID_3:4;
A4: euc2cpx p2 <> euc2cpx p1 by A2, EUCLID_3:4;
assume that
A5: p5 <> p6 and
A6: p5 <> p4 and
A7: p6 <> p4 ; :: thesis: ( not angle (p1,p2,p3) <> PI or not angle (p2,p3,p1) <> PI or not angle (p3,p1,p2) <> PI or not angle (p4,p5,p6) <> PI or not angle (p5,p6,p4) <> PI or not angle (p6,p4,p5) <> PI or not angle (p1,p2,p3) = angle (p4,p5,p6) or not angle (p3,p1,p2) = angle (p6,p4,p5) or |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| )
A8: ( euc2cpx p5 <> euc2cpx p6 & euc2cpx p5 <> euc2cpx p4 ) by A5, A6, EUCLID_3:4;
A9: euc2cpx p6 <> euc2cpx p4 by A7, EUCLID_3:4;
assume A10: ( angle (p1,p2,p3) <> PI & angle (p2,p3,p1) <> PI & angle (p3,p1,p2) <> PI ) ; :: thesis: ( not angle (p4,p5,p6) <> PI or not angle (p5,p6,p4) <> PI or not angle (p6,p4,p5) <> PI or not angle (p1,p2,p3) = angle (p4,p5,p6) or not angle (p3,p1,p2) = angle (p6,p4,p5) or |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| )
assume A11: ( angle (p4,p5,p6) <> PI & angle (p5,p6,p4) <> PI & angle (p6,p4,p5) <> PI ) ; :: thesis: ( not angle (p1,p2,p3) = angle (p4,p5,p6) or not angle (p3,p1,p2) = angle (p6,p4,p5) or |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| )
assume that
A12: angle (p1,p2,p3) = angle (p4,p5,p6) and
A13: angle (p3,p1,p2) = angle (p6,p4,p5) ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|
A14: (sin (angle (p2,p1,p3))) * (sin (angle (p6,p5,p4))) = (sin (angle (p2,p1,p3))) * (- (sin (angle (p1,p2,p3)))) by A12, Th2
.= (- (sin (angle (p6,p4,p5)))) * (- (sin (angle (p1,p2,p3)))) by A13, Th2
.= (sin (angle (p5,p4,p6))) * (- (sin (angle (p1,p2,p3)))) by Th2
.= (sin (angle (p3,p2,p1))) * (sin (angle (p5,p4,p6))) by Th2 ;
per cases ( (sin (angle (p3,p2,p1))) * (sin (angle (p5,p4,p6))) <> 0 or (sin (angle (p3,p2,p1))) * (sin (angle (p5,p4,p6))) = 0 ) ;
suppose A15: (sin (angle (p3,p2,p1))) * (sin (angle (p5,p4,p6))) <> 0 ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|
A16: ((|.(p3 - p2).| * |.(p4 - p6).|) * (sin (angle (p3,p2,p1)))) * (sin (angle (p5,p4,p6))) = (|.(p3 - p2).| * (sin (angle (p3,p2,p1)))) * (|.(p4 - p6).| * (sin (angle (p5,p4,p6))))
.= (|.(p3 - p1).| * (sin (angle (p2,p1,p3)))) * (|.(p4 - p6).| * (sin (angle (p5,p4,p6)))) by A2, Th6
.= (|.(p3 - p1).| * (sin (angle (p2,p1,p3)))) * (|.(p6 - p4).| * (sin (angle (p5,p4,p6)))) by Lm2
.= (|.(p3 - p1).| * (sin (angle (p2,p1,p3)))) * (|.(p6 - p5).| * (sin (angle (p6,p5,p4)))) by A6, Th6
.= ((|.(p3 - p1).| * |.(p6 - p5).|) * (sin (angle (p2,p1,p3)))) * (sin (angle (p6,p5,p4))) ;
thus |.(p3 - p2).| * |.(p4 - p6).| = ((|.(p3 - p2).| * |.(p4 - p6).|) * ((sin (angle (p3,p2,p1))) * (sin (angle (p5,p4,p6))))) / ((sin (angle (p3,p2,p1))) * (sin (angle (p5,p4,p6)))) by A15, XCMPLX_1:89
.= ((|.(p3 - p1).| * |.(p6 - p5).|) * ((sin (angle (p2,p1,p3))) * (sin (angle (p6,p5,p4))))) / ((sin (angle (p3,p2,p1))) * (sin (angle (p5,p4,p6)))) by A16
.= |.(p3 - p1).| * |.(p6 - p5).| by A14, A15, XCMPLX_1:89
.= |.(p1 - p3).| * |.(p6 - p5).| by Lm2 ; :: thesis: verum
end;
suppose A17: (sin (angle (p3,p2,p1))) * (sin (angle (p5,p4,p6))) = 0 ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|
per cases ( sin (angle (p3,p2,p1)) = 0 or sin (angle (p5,p4,p6)) = 0 ) by A17;
suppose A18: sin (angle (p3,p2,p1)) = 0 ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|
A19: ( (2 * PI) * 0 <= angle (p1,p2,p3) & angle (p1,p2,p3) < (2 * PI) + ((2 * PI) * 0) ) by COMPLEX2:70;
- (sin (angle (p1,p2,p3))) = 0 by A18, Th2;
then ( angle (p1,p2,p3) = (2 * PI) * 0 or angle (p1,p2,p3) = PI + ((2 * PI) * 0) ) by A19, SIN_COS6:21;
hence |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| by A3, A4, A10, COMPLEX2:87; :: thesis: verum
end;
suppose A20: sin (angle (p5,p4,p6)) = 0 ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|
A21: ( (2 * PI) * 0 <= angle (p6,p4,p5) & angle (p6,p4,p5) < (2 * PI) + ((2 * PI) * 0) ) by COMPLEX2:70;
- (sin (angle (p6,p4,p5))) = 0 by A20, Th2;
then ( angle (p6,p4,p5) = (2 * PI) * 0 or angle (p6,p4,p5) = PI + ((2 * PI) * 0) ) by A21, SIN_COS6:21;
hence |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| by A8, A9, A11, COMPLEX2:87; :: thesis: verum
end;
end;
end;
end;