let z1, z2 be Complex; |.(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 Th8
.=
(((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:63;
then A3:
((((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:19;
((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= |.(((Re z1) * (Re z2)) + ((Im z1) * (Im z2))).|
by Lm29;
then A4:
((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2)
by Lm28;
A5:
0 <= ((Re z2) ^2) + ((Im z2) ^2)
by Lm1;
then A6:
(sqrt (((Re z2) ^2) + ((Im z2) ^2))) ^2 = ((Re z2) ^2) + ((Im z2) ^2)
by SQUARE_1:def 2;
0 <= (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2
by XREAL_1:63;
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 A3, SQUARE_1:26;
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, A5, SQUARE_1:29;
then A7:
((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= (sqrt (((Re z1) ^2) + ((Im z1) ^2))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2)))
by A4, 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 A7, XREAL_1:64;
then A8:
(((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:7;
(Re (z1 + z2)) ^2 =
((Re z1) + (Re z2)) ^2
by Th8
.=
(((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 A9:
((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 A8, XREAL_1:7;
A10:
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 2;
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 A6, A9, A10, SQUARE_1:26;
hence
|.(z1 + z2).| <= |.z1.| + |.z2.|
by SQUARE_1:22; verum