let p1, p2, p3 be Point of (TOP-REAL 2); ( 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 that
A1:
p1 <> p2
and
A2:
p3 <> p2
; ( |((p1 - p2),(p3 - p2))| = 0 iff ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) )
p1 - p2 <> 0. (TOP-REAL 2)
by A1, RLVECT_1:21;
then A3:
euc2cpx (p1 - p2) <> 0c
by Th2, Th16;
p3 - p2 <> 0. (TOP-REAL 2)
by A2, RLVECT_1:21;
then A4:
euc2cpx (p3 - p2) <> 0c
by Th2, Th16;
A5:
( (euc2cpx p1) - (euc2cpx p2) = euc2cpx (p1 - p2) & (euc2cpx p3) - (euc2cpx p2) = euc2cpx (p3 - p2) )
by Th15;
hereby ( ( 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
;
( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI )then
Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2))) = 0
by Th42;
then
(
angle (
(euc2cpx (p1 - p2)),
0c,
(euc2cpx (p3 - p2)))
= PI / 2 or
angle (
(euc2cpx (p1 - p2)),
0c,
(euc2cpx (p3 - p2)))
= (3 / 2) * PI )
by A3, A4, COMPLEX2:75;
hence
(
angle (
p1,
p2,
p3)
= PI / 2 or
angle (
p1,
p2,
p3)
= (3 / 2) * PI )
by A5, COMPLEX2:71;
verum
end;
A6:
|((p1 - p2),(p3 - p2))| = Re ((euc2cpx (p1 - p2)) .|. (euc2cpx (p3 - p2)))
by Th42;
assume
( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI )
; |((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 A5, COMPLEX2:71;
hence
|((p1 - p2),(p3 - p2))| = 0
by A6, A3, A4, COMPLEX2:75; verum