let p1, p2 be Point of (TOP-REAL 2); ( 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.|) ) ) )
A1:
( p2 `1 = Re (euc2cpx p2) & p2 `2 = Im (euc2cpx p2) )
by COMPLEX1:12;
( p1 `1 = Re (euc2cpx p1) & p1 `2 = Im (euc2cpx p1) )
by COMPLEX1:12;
then A2:
Im ((euc2cpx p1) .|. (euc2cpx p2)) = (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1))
by A1, Th40;
assume
( p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) )
; ( ( ( 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 A3:
( euc2cpx p1 <> 0c & euc2cpx p2 <> 0c )
by Th2, Th16;
( |.(euc2cpx p1).| = |.p1.| & |.(euc2cpx p2).| = |.p2.| )
by Th25;
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 A3, A2, Th17, COMPLEX2:76; verum