let z1, z2 be Quaternion; |.(z1 + z2).| <= |.z1.| + |.z2.|
set m1 = Rea z1;
set m2 = Im1 z1;
set m3 = Im2 z1;
set m4 = Im3 z1;
set n1 = Rea z2;
set n2 = Im1 z2;
set n3 = Im2 z2;
set n4 = Im3 z2;
set a = ((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2);
set b = ((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2);
A1:
|.z1.| >= 0
by Th60;
|.z2.| >= 0
by Th60;
then A2:
|.z1.| + |.z2.| >= 0
by A1;
A3:
((sqrt (((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2))) + (sqrt (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2)))) ^2 = (((((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) + ((Rea z2) ^2)) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2)) + (2 * (sqrt ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) * (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2)))))
by Lm32;
A4:
(sqrt ((((((Rea z1) + (Rea z2)) ^2) + (((Im1 z1) + (Im1 z2)) ^2)) + (((Im2 z1) + (Im2 z2)) ^2)) + (((Im3 z1) + (Im3 z2)) ^2))) ^2 = (((((Rea z1) + (Rea z2)) ^2) + (((Im1 z1) + (Im1 z2)) ^2)) + (((Im2 z1) + (Im2 z2)) ^2)) + (((Im3 z1) + (Im3 z2)) ^2)
by Lm33;
A5:
Rea (z1 + z2) = (Rea z1) + (Rea z2)
by Th29;
A6:
Im1 (z1 + z2) = (Im1 z1) + (Im1 z2)
by Th29;
A7:
Im2 (z1 + z2) = (Im2 z1) + (Im2 z2)
by Th29;
A8:
Im3 (z1 + z2) = (Im3 z1) + (Im3 z2)
by Th29;
A9:
(((Rea z1) * (Im1 z2)) ^2) + (((Im1 z1) * (Rea z2)) ^2) >= (2 * ((Rea z1) * (Im1 z2))) * ((Im1 z1) * (Rea z2))
by SERIES_3:6;
A10:
(((Rea z1) * (Im2 z2)) ^2) + (((Im2 z1) * (Rea z2)) ^2) >= (2 * ((Rea z1) * (Im2 z2))) * ((Im2 z1) * (Rea z2))
by SERIES_3:6;
A11:
(((Rea z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Rea z2)) ^2) >= (2 * ((Rea z1) * (Im3 z2))) * ((Im3 z1) * (Rea z2))
by SERIES_3:6;
A12:
(((Im1 z1) * (Im2 z2)) ^2) + (((Im2 z1) * (Im1 z2)) ^2) >= (2 * ((Im1 z1) * (Im2 z2))) * ((Im2 z1) * (Im1 z2))
by SERIES_3:6;
A13:
(((Im1 z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Im1 z2)) ^2) >= (2 * ((Im1 z1) * (Im3 z2))) * ((Im3 z1) * (Im1 z2))
by SERIES_3:6;
A14:
(((Im2 z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Im2 z2)) ^2) >= (2 * ((Im2 z1) * (Im3 z2))) * ((Im3 z1) * (Im2 z2))
by SERIES_3:6;
set a1 = ((Rea z1) * (Im1 z2)) ^2 ;
set a2 = ((Im1 z1) * (Rea z2)) ^2 ;
set a3 = ((Rea z1) * (Im2 z2)) ^2 ;
set a4 = ((Im2 z1) * (Rea z2)) ^2 ;
set a5 = ((Rea z1) * (Im3 z2)) ^2 ;
set a6 = ((Im3 z1) * (Rea z2)) ^2 ;
set a7 = ((Im1 z1) * (Im2 z2)) ^2 ;
set a8 = ((Im2 z1) * (Im1 z2)) ^2 ;
set a9 = ((Im1 z1) * (Im3 z2)) ^2 ;
set a10 = ((Im3 z1) * (Im1 z2)) ^2 ;
set a11 = ((Im2 z1) * (Im3 z2)) ^2 ;
set a12 = ((Im3 z1) * (Im2 z2)) ^2 ;
set b1 = (2 * ((Rea z1) * (Im1 z2))) * ((Im1 z1) * (Rea z2));
set b2 = (2 * ((Rea z1) * (Im2 z2))) * ((Im2 z1) * (Rea z2));
set b3 = (2 * ((Rea z1) * (Im3 z2))) * ((Im3 z1) * (Rea z2));
set b4 = (2 * ((Im1 z1) * (Im2 z2))) * ((Im2 z1) * (Im1 z2));
set b5 = (2 * ((Im1 z1) * (Im3 z2))) * ((Im3 z1) * (Im1 z2));
set b6 = (2 * ((Im2 z1) * (Im3 z2))) * ((Im3 z1) * (Im2 z2));
((((((((Rea z1) * (Im1 z2)) ^2) + (((Im1 z1) * (Rea z2)) ^2)) + ((((Rea z1) * (Im2 z2)) ^2) + (((Im2 z1) * (Rea z2)) ^2))) + ((((Rea z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Rea z2)) ^2))) + ((((Im1 z1) * (Im2 z2)) ^2) + (((Im2 z1) * (Im1 z2)) ^2))) + ((((Im1 z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Im1 z2)) ^2))) + ((((Im2 z1) * (Im3 z2)) ^2) + (((Im3 z1) * (Im2 z2)) ^2)) >= ((((((2 * ((Rea z1) * (Im1 z2))) * ((Im1 z1) * (Rea z2))) + ((2 * ((Rea z1) * (Im2 z2))) * ((Im2 z1) * (Rea z2)))) + ((2 * ((Rea z1) * (Im3 z2))) * ((Im3 z1) * (Rea z2)))) + ((2 * ((Im1 z1) * (Im2 z2))) * ((Im2 z1) * (Im1 z2)))) + ((2 * ((Im1 z1) * (Im3 z2))) * ((Im3 z1) * (Im1 z2)))) + ((2 * ((Im2 z1) * (Im3 z2))) * ((Im3 z1) * (Im2 z2)))
by A9, A10, A11, A12, A13, A14, Lm30;
then
((((((((((((((Rea z1) * (Im1 z2)) ^2) + (((Im1 z1) * (Rea z2)) ^2)) + (((Rea z1) * (Im2 z2)) ^2)) + (((Im2 z1) * (Rea z2)) ^2)) + (((Rea z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Rea z2)) ^2)) + (((Im1 z1) * (Im2 z2)) ^2)) + (((Im2 z1) * (Im1 z2)) ^2)) + (((Im1 z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Im1 z2)) ^2)) + (((Im2 z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Im2 z2)) ^2)) + ((((((Rea z1) * (Rea z2)) ^2) + (((Im1 z1) * (Im1 z2)) ^2)) + (((Im2 z1) * (Im2 z2)) ^2)) + (((Im3 z1) * (Im3 z2)) ^2)) >= (((((((2 * ((Rea z1) * (Im1 z2))) * ((Im1 z1) * (Rea z2))) + ((2 * ((Rea z1) * (Im2 z2))) * ((Im2 z1) * (Rea z2)))) + ((2 * ((Rea z1) * (Im3 z2))) * ((Im3 z1) * (Rea z2)))) + ((2 * ((Im1 z1) * (Im2 z2))) * ((Im2 z1) * (Im1 z2)))) + ((2 * ((Im1 z1) * (Im3 z2))) * ((Im3 z1) * (Im1 z2)))) + ((2 * ((Im2 z1) * (Im3 z2))) * ((Im3 z1) * (Im2 z2)))) + ((((((Rea z1) * (Rea z2)) ^2) + (((Im1 z1) * (Im1 z2)) ^2)) + (((Im2 z1) * (Im2 z2)) ^2)) + (((Im3 z1) * (Im3 z2)) ^2))
by XREAL_1:6;
then
((((((((((((((Rea z1) * (Im1 z2)) ^2) + (((Im1 z1) * (Rea z2)) ^2)) + (((Rea z1) * (Im2 z2)) ^2)) + (((Im2 z1) * (Rea z2)) ^2)) + (((Rea z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Rea z2)) ^2)) + (((Im1 z1) * (Im2 z2)) ^2)) + (((Im2 z1) * (Im1 z2)) ^2)) + (((Im1 z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Im1 z2)) ^2)) + (((Im2 z1) * (Im3 z2)) ^2)) + (((Im3 z1) * (Im2 z2)) ^2)) + ((((((Rea z1) * (Rea z2)) ^2) + (((Im1 z1) * (Im1 z2)) ^2)) + (((Im2 z1) * (Im2 z2)) ^2)) + (((Im3 z1) * (Im3 z2)) ^2)) >= (((((Rea z1) * (Rea z2)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z1) * (Im2 z2))) + ((Im3 z1) * (Im3 z2))) ^2
;
then
sqrt ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) * (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2))) >= ((((Rea z1) * (Rea z2)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z1) * (Im2 z2))) + ((Im3 z1) * (Im3 z2))
by Lm29;
then
2 * (sqrt ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) * (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2)))) >= 2 * (((((Rea z1) * (Rea z2)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z1) * (Im2 z2))) + ((Im3 z1) * (Im3 z2)))
by XREAL_1:64;
then
((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) + (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2))) + (2 * (sqrt ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) * (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2))))) >= ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) + (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2))) + (2 * (((((Rea z1) * (Rea z2)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z1) * (Im2 z2))) + ((Im3 z1) * (Im3 z2))))
by XREAL_1:6;
hence
|.(z1 + z2).| <= |.z1.| + |.z2.|
by A2, A3, A4, A5, A6, A7, A8, Lm31; verum