let z1, z2 be Complex; ( (Re z1) * (Im z2) = (Re z2) * (Im z1) & ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0 implies |.(z1 + z2).| = |.z1.| + |.z2.| )
assume that
A1:
(Re z1) * (Im z2) = (Re z2) * (Im z1)
and
A2:
((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0
; |.(z1 + z2).| = |.z1.| + |.z2.|
set r1 = Re z1;
set r2 = Re z2;
set i1 = Im z1;
set i2 = Im z2;
A3: (Re (z1 + z2)) ^2 =
((Re z1) + (Re z2)) ^2
by COMPLEX1:8
.=
(((Re z1) ^2) + ((2 * (Re z1)) * (Re z2))) + ((Re z2) ^2)
;
((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) = |.(((Re z1) * (Re z2)) + ((Im z1) * (Im z2))).|
by A2, ABSVALUE:def 1;
then A4:
((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) = sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2)
by COMPLEX1:72;
A5: (Im (z1 + z2)) ^2 =
((Im z1) + (Im z2)) ^2
by COMPLEX1:8
.=
(((Im z1) ^2) + ((2 * (Im z1)) * (Im z2))) + ((Im z2) ^2)
;
A6:
0 <= ((Re z2) ^2) + ((Im z2) ^2)
by Lm2;
then A7:
(sqrt (((Re z2) ^2) + ((Im z2) ^2))) ^2 = ((Re z2) ^2) + ((Im z2) ^2)
by SQUARE_1:def 2;
A8:
0 <= sqrt (((Re z2) ^2) + ((Im z2) ^2))
by A6, SQUARE_1:def 2;
A9:
0 <= ((Re z1) ^2) + ((Im z1) ^2)
by Lm2;
then
0 <= sqrt (((Re z1) ^2) + ((Im z1) ^2))
by SQUARE_1:def 2;
then A10:
0 + 0 <= (sqrt (((Re z1) ^2) + ((Im z1) ^2))) + (sqrt (((Re z2) ^2) + ((Im z2) ^2)))
by A8;
((((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2))) - ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) = (((Re z1) * (Im z2)) - ((Im z1) * (Re z2))) ^2
;
then
sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) = sqrt ((((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2)))
by A1, XCMPLX_1:15;
then A11:
sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) = (sqrt (((Re z1) ^2) + ((Im z1) ^2))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2)))
by A9, A6, SQUARE_1:29;
(sqrt (((Re z1) ^2) + ((Im z1) ^2))) ^2 = ((Re z1) ^2) + ((Im z1) ^2)
by A9, SQUARE_1:def 2;
then
sqrt (((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2)) = sqrt (((sqrt (((Re z1) ^2) + ((Im z1) ^2))) + (sqrt (((Re z2) ^2) + ((Im z2) ^2)))) ^2)
by A7, A3, A5, A4, A11;
then
sqrt (((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2)) = (sqrt (((Re z1) ^2) + ((Im z1) ^2))) + (sqrt (((Re z2) ^2) + ((Im z2) ^2)))
by A10, SQUARE_1:22;
then
sqrt (((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2)) = (sqrt (((Re z1) ^2) + ((Im z1) ^2))) + |.z2.|
by COMPLEX1:def 12;
then
sqrt (((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2)) = |.z1.| + |.z2.|
by COMPLEX1:def 12;
hence
|.(z1 + z2).| = |.z1.| + |.z2.|
by COMPLEX1:def 12; verum