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;
((((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;
(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 SQUARE_1:89; verum