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:19
.=
(((Re z1) ^2 ) + ((2 * (Re z1)) * (Re z2))) + ((Re z2) ^2 )
;
((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) = abs (((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:158;
A5: (Im (z1 + z2)) ^2 =
((Im z1) + (Im z2)) ^2
by COMPLEX1:19
.=
(((Im z1) ^2 ) + ((2 * (Im z1)) * (Im z2))) + ((Im z2) ^2 )
;
A6:
0 <= ((Re z2) ^2 ) + ((Im z2) ^2 )
by Lm3;
then A7:
(sqrt (((Re z2) ^2 ) + ((Im z2) ^2 ))) ^2 = ((Re z2) ^2 ) + ((Im z2) ^2 )
by SQUARE_1:def 4;
A8:
0 <= sqrt (((Re z2) ^2 ) + ((Im z2) ^2 ))
by A6, SQUARE_1:def 4;
A9:
0 <= ((Re z1) ^2 ) + ((Im z1) ^2 )
by Lm3;
then
0 <= sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))
by SQUARE_1:def 4;
then A10:
0 + 0 <= (sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))) + (sqrt (((Re z2) ^2 ) + ((Im z2) ^2 )))
by A8, XREAL_1:9;
((((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:97;
(sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))) ^2 = ((Re z1) ^2 ) + ((Im z1) ^2 )
by A9, SQUARE_1:def 4;
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:89;
then
sqrt (((Re (z1 + z2)) ^2 ) + ((Im (z1 + z2)) ^2 )) = (sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))) + |.z2.|
by COMPLEX1:def 16;
then
sqrt (((Re (z1 + z2)) ^2 ) + ((Im (z1 + z2)) ^2 )) = |.z1.| + |.z2.|
by COMPLEX1:def 16;
hence
|.(z1 + z2).| = |.z1.| + |.z2.|
by COMPLEX1:def 16; verum