let z1, z2 be quaternion number ; :: thesis: |.(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 );
( |.z1.| >= 0 & |.z2.| >= 0 & |.(z1 + z2).| >= 0 ) by Th67;
then A1: |.z1.| + |.z2.| >= 0 ;
A2: ((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 Lm29;
A3: (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 Lm30;
A4: ( Rea (z1 + z2) = (Rea z1) + (Rea z2) & Im1 (z1 + z2) = (Im1 z1) + (Im1 z2) & Im2 (z1 + z2) = (Im2 z1) + (Im2 z2) & Im3 (z1 + z2) = (Im3 z1) + (Im3 z2) ) by Lm25;
A5: ( (((Rea z1) * (Im1 z2)) ^2 ) + (((Im1 z1) * (Rea z2)) ^2 ) >= (2 * ((Rea z1) * (Im1 z2))) * ((Im1 z1) * (Rea z2)) & (((Rea z1) * (Im2 z2)) ^2 ) + (((Im2 z1) * (Rea z2)) ^2 ) >= (2 * ((Rea z1) * (Im2 z2))) * ((Im2 z1) * (Rea z2)) & (((Rea z1) * (Im3 z2)) ^2 ) + (((Im3 z1) * (Rea z2)) ^2 ) >= (2 * ((Rea z1) * (Im3 z2))) * ((Im3 z1) * (Rea z2)) & (((Im1 z1) * (Im2 z2)) ^2 ) + (((Im2 z1) * (Im1 z2)) ^2 ) >= (2 * ((Im1 z1) * (Im2 z2))) * ((Im2 z1) * (Im1 z2)) & (((Im1 z1) * (Im3 z2)) ^2 ) + (((Im3 z1) * (Im1 z2)) ^2 ) >= (2 * ((Im1 z1) * (Im3 z2))) * ((Im3 z1) * (Im1 z2)) & (((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 A5, Lm27;
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 Lm26;
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 A1, A2, A3, A4, Lm28; :: thesis: verum