let n be Element of NAT ; :: thesis: for z1, z2 being Element of COMPLEX n holds |.(z1 + z2).| <= |.z1.| + |.z2.|
let z1, z2 be Element of COMPLEX n; :: thesis: |.(z1 + z2).| <= |.z1.| + |.z2.|
A1: ( 0 <= Sum (sqr (abs z1)) & 0 <= Sum (sqr (abs z2)) ) by RVSUM_1:116;
then A2: ( 0 <= sqrt (Sum (sqr (abs z1))) & 0 <= sqrt (Sum (sqr (abs z2))) ) by SQUARE_1:def 4;
A3: Sum (sqr ((abs z1) + (abs z2))) = Sum (((sqr (abs z1)) + (2 * (mlt (abs z1),(abs z2)))) + (sqr (abs z2))) by RVSUM_1:98
.= (Sum ((sqr (abs z1)) + (2 * (mlt (abs z1),(abs z2))))) + (Sum (sqr (abs z2))) by RVSUM_1:119
.= ((Sum (sqr (abs z1))) + (Sum (2 * (mlt (abs z1),(abs z2))))) + (Sum (sqr (abs z2))) by RVSUM_1:119
.= ((Sum (sqr (abs z1))) + (2 * (Sum (mlt (abs z1),(abs z2))))) + (Sum (sqr (abs z2))) by RVSUM_1:117 ;
for k being Nat st k in Seg n holds
(sqr (abs (z1 + z2))) . k <= (sqr ((abs z1) + (abs z2))) . k

proof

let k be Nat; :: thesis: ( k in Seg n implies (sqr (abs (z1 + z2))) . k <= (sqr ((abs z1) + (abs z2))) . k )
assume A4: k in Seg n ; :: thesis: (sqr (abs (z1 + z2))) . k <= (sqr ((abs z1) + (abs z2))) . k
set r2 = (sqr ((abs z1) + (abs z2))) . k;
reconsider c1 = z1 . k, c2 = z2 . k as Element of COMPLEX by A4, Th21;
reconsider c12 = (z1 + z2) . k as Element of COMPLEX by A4, Th21;
reconsider abs1 = (abs z1) . k, abs2 = (abs z2) . k as Real by A4, Lm5;
reconsider abs12 = ((abs z1) + (abs z2)) . k as Real by A4, Lm5;
reconsider abs'12 = (abs (z1 + z2)) . k as Real by A4, Lm5;
|.(c1 + c2).| <= |.c1.| + |.c2.| by COMPLEX1:142;
then |.c12.| <= |.c1.| + |.c2.| by A4, Th24;
then |.c12.| <= |.c1.| + abs2 by A4, Th59;
then A5: |.c12.| <= abs1 + abs2 by A4, Th59;
len ((abs z1) + (abs z2)) = n by FINSEQ_1:def 18;
then dom ((abs z1) + (abs z2)) = Seg n by FINSEQ_1:def 3;
then ( 0 <= |.c12.| & |.c12.| <= abs12 ) by A4, A5, COMPLEX1:132, VALUED_1:def 1;
then ( abs'12 <= abs12 & 0 <= abs'12 ) by A4, Th59;
then abs'12 ^2 <= abs12 ^2 by SQUARE_1:77;
then abs'12 ^2 <= (sqr ((abs z1) + (abs z2))) . k by VALUED_1:11;
hence (sqr (abs (z1 + z2))) . k <= (sqr ((abs z1) + (abs z2))) . k by VALUED_1:11; :: thesis: verum

end;

then A6: Sum (sqr (abs (z1 + z2))) <= ((Sum (sqr (abs z1))) + (2 * (Sum (mlt (abs z1),(abs z2))))) + (Sum (sqr (abs z2))) by A3, RVSUM_1:112;
A7: for k being Nat st k in Seg n holds
0 <= (mlt (abs z1),(abs z2)) . k

proof

let k be Nat; :: thesis: ( k in Seg n implies 0 <= (mlt (abs z1),(abs z2)) . k )
assume A8: k in Seg n ; :: thesis: 0 <= (mlt (abs z1),(abs z2)) . k
set r = (mlt (abs z1),(abs z2)) . k;
reconsider c1 = z1 . k, c2 = z2 . k as Element of COMPLEX by A8, Th21;
( len (mlt (abs z1),(abs z2)) = n & (abs z1) . k = |.c1.| & (abs z2) . k = |.c2.| ) by A8, Th59, FINSEQ_1:def 18;
then ( (mlt (abs z1),(abs z2)) . k = |.c1.| * |.c2.| & 0 <= |.c1.| & 0 <= |.c2.| ) by COMPLEX1:132, RVSUM_1:87;
then 0 * |.c2.| <= (mlt (abs z1),(abs z2)) . k ;
hence 0 <= (mlt (abs z1),(abs z2)) . k ; :: thesis: verum

end;

len (mlt (abs z1),(abs z2)) = n by FINSEQ_1:def 18;
then ( dom (mlt (abs z1),(abs z2)) = Seg n & 0 <= (Sum (mlt (abs z1),(abs z2))) ^2 & (Sum (mlt (abs z1),(abs z2))) ^2 <= (Sum (sqr (abs z1))) * (Sum (sqr (abs z2))) ) by FINSEQ_1:def 3, RVSUM_1:122, XREAL_1:65;
then ( 0 <= Sum (mlt (abs z1),(abs z2)) & sqrt ((Sum (mlt (abs z1),(abs z2))) ^2 ) <= sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2)))) ) by A7, RVSUM_1:114, SQUARE_1:94;
then ( 0 <= 2 & Sum (mlt (abs z1),(abs z2)) <= sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2)))) ) by SQUARE_1:89;
then ( Sum (sqr (abs z1)) <= Sum (sqr (abs z1)) & 2 * (Sum (mlt (abs z1),(abs z2))) <= 2 * (sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2))))) ) by XREAL_1:66;
then ( Sum (sqr (abs z2)) <= Sum (sqr (abs z2)) & (Sum (sqr (abs z1))) + (2 * (Sum (mlt (abs z1),(abs z2)))) <= (Sum (sqr (abs z1))) + (2 * (sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2)))))) ) by XREAL_1:9;
then ((Sum (sqr (abs z1))) + (2 * (Sum (mlt (abs z1),(abs z2))))) + (Sum (sqr (abs z2))) <= ((Sum (sqr (abs z1))) + (2 * (sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2))))))) + (Sum (sqr (abs z2))) by XREAL_1:9;
then Sum (sqr (abs (z1 + z2))) <= ((Sum (sqr (abs z1))) + (2 * (sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2))))))) + (Sum (sqr (abs z2))) by A6, XXREAL_0:2;
then Sum (sqr (abs (z1 + z2))) <= ((Sum (sqr (abs z1))) + (2 * ((sqrt (Sum (sqr (abs z1)))) * (sqrt (Sum (sqr (abs z2))))))) + (Sum (sqr (abs z2))) by A1, SQUARE_1:97;
then ( Sum (sqr (abs z1)) = (sqrt (Sum (sqr (abs z1)))) ^2 & (sqrt (Sum (sqr (abs z2)))) ^2 = Sum (sqr (abs z2)) & Sum (sqr (abs (z1 + z2))) <= ((Sum (sqr (abs z1))) + ((2 * (sqrt (Sum (sqr (abs z1))))) * (sqrt (Sum (sqr (abs z2)))))) + (Sum (sqr (abs z2))) ) by A1, SQUARE_1:def 4;
then ( 0 <= Sum (sqr (abs (z1 + z2))) & Sum (sqr (abs (z1 + z2))) <= ((sqrt (Sum (sqr (abs z1)))) + (sqrt (Sum (sqr (abs z2))))) ^2 ) by RVSUM_1:116;
then ( 0 + 0 <= (sqrt (Sum (sqr (abs z1)))) + (sqrt (Sum (sqr (abs z2)))) & sqrt (Sum (sqr (abs (z1 + z2)))) <= sqrt (((sqrt (Sum (sqr (abs z1)))) + (sqrt (Sum (sqr (abs z2))))) ^2 ) ) by A2, SQUARE_1:94;
hence |.(z1 + z2).| <= |.z1.| + |.z2.| by SQUARE_1:89; :: thesis: verum