let z1, z2 be complex number ; |.(z1 + z2).| <= |.z1.| + |.z2.|
set r1 = Re z1;
set r2 = Re z2;
set i1 = Im z1;
set i2 = Im z2;
A1: (Im (z1 + z2)) ^2 =
((Im z1) + (Im z2)) ^2
by Th19
.=
(((Im z1) ^2 ) + ((2 * (Im z1)) * (Im z2))) + ((Im z2) ^2 )
;
A2:
0 <= ((Re z1) ^2 ) + ((Im z1) ^2 )
by Lm1;
then A3:
0 <= sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))
by SQUARE_1:def 4;
((((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 A4:
((((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;
((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= |.(((Re z1) * (Re z2)) + ((Im z1) * (Im z2))).|
by Lm25;
then A5:
((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2 )
by Lm24;
A6:
0 <= ((Re z2) ^2 ) + ((Im z2) ^2 )
by Lm1;
then A7:
(sqrt (((Re z2) ^2 ) + ((Im z2) ^2 ))) ^2 = ((Re z2) ^2 ) + ((Im z2) ^2 )
by SQUARE_1:def 4;
0 <= (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2
by XREAL_1:65;
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 A4, SQUARE_1:94;
then
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 A2, A6, SQUARE_1:97;
then A8:
((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= (sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))) * (sqrt (((Re z2) ^2 ) + ((Im z2) ^2 )))
by A5, XXREAL_0:2;
((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2)) = 2 * (((Re z1) * (Re z2)) + ((Im z1) * (Im z2)))
;
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 A8, XREAL_1:66;
then A9:
(((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 ))))
by XREAL_1:9;
(Re (z1 + z2)) ^2 =
((Re z1) + (Re z2)) ^2
by Th19
.=
(((Re z1) ^2 ) + ((2 * (Re z1)) * (Re z2))) + ((Re z2) ^2 )
;
then
((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 A1;
then A10:
((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 A9, XREAL_1:9;
A11:
0 <= ((Re (z1 + z2)) ^2 ) + ((Im (z1 + z2)) ^2 )
by Lm1;
A12:
0 <= sqrt (((Re z2) ^2 ) + ((Im z2) ^2 ))
by A6, SQUARE_1:def 4;
(sqrt (((Re z1) ^2 ) + ((Im z1) ^2 ))) ^2 = ((Re z1) ^2 ) + ((Im z1) ^2 )
by A2, 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, A10, A11, SQUARE_1:94;
hence
|.(z1 + z2).| <= |.z1.| + |.z2.|
by A3, A12, SQUARE_1:89; verum