let x, y, z be Complex; ( x <> y & z <> y & ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) implies (|.(x - y).| ^2) + (|.(z - y).| ^2) = |.(x - z).| ^2 )
assume A1:
( x <> y & z <> y & ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) )
; (|.(x - y).| ^2) + (|.(z - y).| ^2) = |.(x - z).| ^2
set x3 = x - z;
A2: (|.(x - y).| ^2) + (|.(z - y).| ^2) =
(Re ((x - y) .|. (x - y))) + (|.(z - y).| ^2)
by Th29
.=
(Re ((x - y) .|. (x - y))) + (Re ((z - y) .|. (z - y)))
by Th29
.=
Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))
by COMPLEX1:8
;
x - z = (x - y) - (z - y)
;
then
(x - z) .|. (x - z) = ((((x - y) .|. (x - y)) - ((x - y) .|. (z - y))) - ((z - y) .|. (x - y))) + ((z - y) .|. (z - y))
by Th47;
then Re ((x - z) .|. (x - z)) =
Re ((((x - y) .|. (x - y)) + ((z - y) .|. (z - y))) - (((x - y) .|. (z - y)) + ((z - y) .|. (x - y))))
.=
(Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - (Re (((x - y) .|. (z - y)) + ((z - y) .|. (x - y))))
by COMPLEX1:19
.=
(Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ((Re ((x - y) .|. (z - y))) + (Re ((z - y) .|. (x - y))))
by COMPLEX1:8
.=
(Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ((Re ((x - y) .|. (z - y))) + (Re (((x - y) .|. (z - y)) *')))
by Th32
.=
(Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ((Re ((x - y) .|. (z - y))) + (Re ((x - y) .|. (z - y))))
by COMPLEX1:27
.=
(Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - (0 + (Re ((x - y) .|. (z - y))))
by A1, Lm3
.=
(Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - 0
by A1, Lm3
.=
Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))
;
hence
(|.(x - y).| ^2) + (|.(z - y).| ^2) = |.(x - z).| ^2
by A2, Th29; verum