let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) implies ( ( ( not (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = |.p1.| * |.p2.| & not (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = - (|.p1.| * |.p2.|) ) or angle p1,(0. (TOP-REAL 2)),p2 = PI / 2 or angle p1,(0. (TOP-REAL 2)),p2 = (3 / 2) * PI ) & ( ( not angle p1,(0. (TOP-REAL 2)),p2 = PI / 2 & not angle p1,(0. (TOP-REAL 2)),p2 = (3 / 2) * PI ) or (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = |.p1.| * |.p2.| or (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = - (|.p1.| * |.p2.|) ) ) )
assume A1: ( p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) ) ; :: thesis: ( ( ( not (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = |.p1.| * |.p2.| & not (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = - (|.p1.| * |.p2.|) ) or angle p1,(0. (TOP-REAL 2)),p2 = PI / 2 or angle p1,(0. (TOP-REAL 2)),p2 = (3 / 2) * PI ) & ( ( not angle p1,(0. (TOP-REAL 2)),p2 = PI / 2 & not angle p1,(0. (TOP-REAL 2)),p2 = (3 / 2) * PI ) or (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = |.p1.| * |.p2.| or (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = - (|.p1.| * |.p2.|) ) )
then A2: euc2cpx p1 <> 0c by Th2, Th20;
A3: euc2cpx p2 <> 0c by A1, Th2, Th20;
A4: ( p1 `1 = Re (euc2cpx p1) & p1 `2 = Im (euc2cpx p1) ) by COMPLEX1:28;
( p2 `1 = Re (euc2cpx p2) & p2 `2 = Im (euc2cpx p2) ) by COMPLEX1:28;
then A5: Im ((euc2cpx p1) .|. (euc2cpx p2)) = (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) by A4, Th49;
A6: |.(euc2cpx p1).| = |.p1.| by Th31;
|.(euc2cpx p2).| = |.p2.| by Th31;
hence ( ( ( not (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = |.p1.| * |.p2.| & not (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = - (|.p1.| * |.p2.|) ) or angle p1,(0. (TOP-REAL 2)),p2 = PI / 2 or angle p1,(0. (TOP-REAL 2)),p2 = (3 / 2) * PI ) & ( ( not angle p1,(0. (TOP-REAL 2)),p2 = PI / 2 & not angle p1,(0. (TOP-REAL 2)),p2 = (3 / 2) * PI ) or (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = |.p1.| * |.p2.| or (- ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 )) = - (|.p1.| * |.p2.|) ) ) by A2, A3, A5, A6, Th21, COMPLEX2:90; :: thesis: verum