let z1, z2 be quaternion number ; |.(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 Th67;
|.z2.| >= 0
by Th67;
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 Lm31;
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 Lm32;
A5:
Rea (z1 + z2) = (Rea z1) + (Rea z2)
by Lm27;
A6:
Im1 (z1 + z2) = (Im1 z1) + (Im1 z2)
by Lm27;
A7:
Im2 (z1 + z2) = (Im2 z1) + (Im2 z2)
by Lm27;
A8:
Im3 (z1 + z2) = (Im3 z1) + (Im3 z2)
by Lm27;
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, Lm29;
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:8;
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 Lm28;
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:66;
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:8;
hence
|.(z1 + z2).| <= |.z1.| + |.z2.|
by A2, A3, A4, A5, A6, A7, A8, Lm30; verum