let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p1 <> p2 & p3 <> p2 implies ( |((p1 - p2),(p3 - p2))| = 0 iff ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI ) ) )
assume A1:
( p1 <> p2 & p3 <> p2 )
; :: thesis: ( |((p1 - p2),(p3 - p2))| = 0 iff ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI ) )
A2:
(euc2cpx p1) - (euc2cpx p2) = euc2cpx (p1 - p2)
by Th19;
A3:
(euc2cpx p3) - (euc2cpx p2) = euc2cpx (p3 - p2)
by Th19;
A4:
|((p1 - p2),(p3 - p2))| = Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))
by Th51;
( p1 - p2 <> 0. (TOP-REAL 2) & p3 - p2 <> 0. (TOP-REAL 2) )
by A1, EUCLID:47;
then A5:
( euc2cpx (p1 - p2) <> 0c & euc2cpx (p3 - p2) <> 0c )
by Th2, Th20;
hereby :: thesis: ( ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI ) implies |((p1 - p2),(p3 - p2))| = 0 )
assume
|((p1 - p2),(p3 - p2))| = 0
;
:: thesis: ( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI )then
Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2))) = 0
by Th51;
then
(
angle (euc2cpx (p1 - p2)),
0c ,
(euc2cpx (p3 - p2)) = PI / 2 or
angle (euc2cpx (p1 - p2)),
0c ,
(euc2cpx (p3 - p2)) = (3 / 2) * PI )
by A5, COMPLEX2:89;
hence
(
angle p1,
p2,
p3 = PI / 2 or
angle p1,
p2,
p3 = (3 / 2) * PI )
by A2, A3, COMPLEX2:85;
:: thesis: verum
end;
assume
( angle p1,p2,p3 = PI / 2 or angle p1,p2,p3 = (3 / 2) * PI )
; :: thesis: |((p1 - p2),(p3 - p2))| = 0
then
( angle (euc2cpx (p1 - p2)),0c ,(euc2cpx (p3 - p2)) = PI / 2 or angle (euc2cpx (p1 - p2)),0c ,(euc2cpx (p3 - p2)) = (3 / 2) * PI )
by A2, A3, COMPLEX2:85;
hence
|((p1 - p2),(p3 - p2))| = 0
by A4, A5, COMPLEX2:89; :: thesis: verum