let z1, z2 be Complex; :: thesis: ( (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 ; :: thesis: |.(z1 + z2).| = |.z1.| + |.z2.|
set r1 = Re z1;
set r2 = Re z2;
set i1 = Im z1;
set i2 = Im z2;
A3: ( 0 <= ((Re z1) ^2 ) + ((Im z1) ^2 ) & 0 <= ((Re z2) ^2 ) + ((Im z2) ^2 ) ) by Lm3;
then A4: ( (sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))) ^2 = ((Re z1) ^2 ) + ((Im z1) ^2 ) & (sqrt (((Re z2) ^2 ) + ((Im z2) ^2 ))) ^2 = ((Re z2) ^2 ) + ((Im z2) ^2 ) ) by SQUARE_1:def 4;
A5: (Re (z1 + z2)) ^2 = ((Re z1) + (Re z2)) ^2 by COMPLEX1:19
.= (((Re z1) ^2 ) + ((2 * (Re z1)) * (Re z2))) + ((Re z2) ^2 ) ;
A6: (Im (z1 + z2)) ^2 = ((Im z1) + (Im z2)) ^2 by COMPLEX1:19
.= (((Im z1) ^2 ) + ((2 * (Im z1)) * (Im z2))) + ((Im z2) ^2 ) ;
((((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 ( ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) = abs (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) & 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, A2, ABSVALUE:def 1, XCMPLX_1:15;
then ( ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) = sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2 ) & 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 A3, COMPLEX1:158, SQUARE_1:97;
then ( 0 <= ((Re (z1 + z2)) ^2 ) + ((Im (z1 + z2)) ^2 ) & 0 <= sqrt (((Re z1) ^2 ) + ((Im z1) ^2 )) & 0 <= sqrt (((Re z2) ^2 ) + ((Im z2) ^2 )) & ((Re (z1 + z2)) ^2 ) + ((Im (z1 + z2)) ^2 ) = ((sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))) + (sqrt (((Re z2) ^2 ) + ((Im z2) ^2 )))) ^2 ) by A3, A4, A5, A6, Lm3, SQUARE_1:def 4;
then ( 0 + 0 <= (sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))) + (sqrt (((Re z2) ^2 ) + ((Im z2) ^2 ))) & 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 XREAL_1:9;
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 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; :: thesis: verum