let z1, z2 be complex number ; :: thesis: |.(z1 + z2).| <= |.z1.| + |.z2.|
set r1 = Re z1;
set r2 = Re z2;
set i1 = Im z1;
set i2 = Im z2;
A1: ( 0 <= ((Re z1) ^2 ) + ((Im z1) ^2 ) & 0 <= ((Re z2) ^2 ) + ((Im z2) ^2 ) ) by Lm2;
then A2: ( (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;
A3: (Re (z1 + z2)) ^2 = ((Re z1) + (Re z2)) ^2 by Th19
.= (((Re z1) ^2 ) + ((2 * (Re z1)) * (Re z2))) + ((Re z2) ^2 ) ;
(Im (z1 + z2)) ^2 = ((Im z1) + (Im z2)) ^2 by Th19
.= (((Im z1) ^2 ) + ((2 * (Im z1)) * (Im z2))) + ((Im z2) ^2 ) ;
then A4: ((Re (z1 + z2)) ^2 ) + ((Im (z1 + z2)) ^2 ) = ((((Re z1) ^2 ) + ((Im z1) ^2 )) + (((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2)))) + (((Re z2) ^2 ) + ((Im z2) ^2 )) by A3;
((((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 0 <= ((((Re z1) ^2 ) + ((Im z1) ^2 )) * (((Re z2) ^2 ) + ((Im z2) ^2 ))) - ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2 ) by XREAL_1:65;
then ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2 ) + 0 <= (((Re z1) ^2 ) + ((Im z1) ^2 )) * (((Re z2) ^2 ) + ((Im z2) ^2 )) by XREAL_1:21;
then ( 0 <= (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2 & (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2 <= (((Re z1) ^2 ) + ((Im z1) ^2 )) * (((Re z2) ^2 ) + ((Im z2) ^2 )) ) by XREAL_1:65;
then ( ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= |.(((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 Lm25, SQUARE_1:94;
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 A1, Lm24, SQUARE_1:97;
then A5: ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= (sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))) * (sqrt (((Re z2) ^2 ) + ((Im z2) ^2 ))) by XXREAL_0:2;
( ((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2)) = 2 * (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) & 0 <= 2 ) ;
then ((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2)) <= 2 * ((sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))) * (sqrt (((Re z2) ^2 ) + ((Im z2) ^2 )))) by A5, XREAL_1:66;
then ( (((Re z1) ^2 ) + ((Im z1) ^2 )) + (((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2))) <= (((Re z1) ^2 ) + ((Im z1) ^2 )) + ((2 * (sqrt (((Re z1) ^2 ) + ((Im z1) ^2 )))) * (sqrt (((Re z2) ^2 ) + ((Im z2) ^2 )))) & ((Re z2) ^2 ) + ((Im z2) ^2 ) <= ((Re z2) ^2 ) + ((Im z2) ^2 ) ) by XREAL_1:9;
then ((Re (z1 + z2)) ^2 ) + ((Im (z1 + z2)) ^2 ) <= ((((Re z1) ^2 ) + ((Im z1) ^2 )) + ((2 * (sqrt (((Re z1) ^2 ) + ((Im z1) ^2 )))) * (sqrt (((Re z2) ^2 ) + ((Im z2) ^2 ))))) + (((Re z2) ^2 ) + ((Im z2) ^2 )) by A4, XREAL_1:9;
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 A2, Lm2, 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 SQUARE_1:94;
hence |.(z1 + z2).| <= |.z1.| + |.z2.| by SQUARE_1:89; :: thesis: verum