let n be 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 + z2))) by RVSUM_1:86;
A2: 0 <= Sum (sqr (abs z1)) by RVSUM_1:86;
then A3: 0 <= sqrt (Sum (sqr (abs z1))) by SQUARE_1:def 2;
A4: 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 )
set r = (mlt ((abs z1),(abs z2))) . k;
assume A5: k in Seg n ; :: thesis: 0 <= (mlt ((abs z1),(abs z2))) . k
then reconsider c1 = z1 . k, c2 = z2 . k as Element of COMPLEX by Th57;
( (abs z1) . k = |.c1.| & (abs z2) . k = |.c2.| ) by A5, Th88;
then A6: (mlt ((abs z1),(abs z2))) . k = |.c1.| * |.c2.| by RVSUM_1:60;
( 0 <= |.c1.| & 0 <= |.c2.| ) by COMPLEX1:46;
hence 0 <= (mlt ((abs z1),(abs z2))) . k by A6; :: thesis: verum

end;

0 <= (Sum (mlt ((abs z1),(abs z2)))) ^2 by XREAL_1:63;
then A7: sqrt ((Sum (mlt ((abs z1),(abs z2)))) ^2) <= sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2)))) by RVSUM_1:92, SQUARE_1:26;
len (mlt ((abs z1),(abs z2))) = n by CARD_1:def 7;
then dom (mlt ((abs z1),(abs z2))) = Seg n by FINSEQ_1:def 3;
then Sum (mlt ((abs z1),(abs z2))) <= sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2)))) by A4, A7, RVSUM_1:84, SQUARE_1:22;
then 2 * (Sum (mlt ((abs z1),(abs z2)))) <= 2 * (sqrt ((Sum (sqr (abs z1))) * (Sum (sqr (abs z2))))) by XREAL_1:64;
then (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:7;
then A8: ((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:7;
A9: 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 )
set r2 = (sqr ((abs z1) + (abs z2))) . k;
len ((abs z1) + (abs z2)) = n by CARD_1:def 7;
then A10: dom ((abs z1) + (abs z2)) = Seg n by FINSEQ_1:def 3;
assume A11: k in Seg n ; :: thesis: (sqr (abs (z1 + z2))) . k <= (sqr ((abs z1) + (abs z2))) . k
then reconsider c12 = (z1 + z2) . k as Element of COMPLEX by Th57;
reconsider abs912 = (abs (z1 + z2)) . k as Real ;
0 <= |.c12.| by COMPLEX1:46;
then A12: 0 <= abs912 by A11, Th88;
reconsider abs1 = (abs z1) . k, abs2 = (abs z2) . k as Real ;
reconsider c1 = z1 . k, c2 = z2 . k as Element of COMPLEX by A11, Th57;
reconsider abs12 = ((abs z1) + (abs z2)) . k as Real ;
|.(c1 + c2).| <= |.c1.| + |.c2.| by COMPLEX1:56;
then |.c12.| <= |.c1.| + |.c2.| by A11, Th58;
then |.c12.| <= |.c1.| + abs2 by A11, Th88;
then |.c12.| <= abs1 + abs2 by A11, Th88;
then |.c12.| <= abs12 by A11, A10, VALUED_1:def 1;
then abs912 <= abs12 by A11, Th88;
then abs912 ^2 <= abs12 ^2 by A12, SQUARE_1:15;
then abs912 ^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;

A13: 0 <= Sum (sqr (abs z2)) by RVSUM_1:86;
then A14: 0 <= sqrt (Sum (sqr (abs z2))) by SQUARE_1:def 2;
A15: Sum (sqr (abs z1)) = (sqrt (Sum (sqr (abs z1)))) ^2 by A2, SQUARE_1:def 2;
A16: (sqrt (Sum (sqr (abs z2)))) ^2 = Sum (sqr (abs z2)) by A13, SQUARE_1:def 2;
Sum (sqr ((abs z1) + (abs z2))) = Sum (((sqr (abs z1)) + (2 * (mlt ((abs z1),(abs z2))))) + (sqr (abs z2))) by RVSUM_1:68
.= (Sum ((sqr (abs z1)) + (2 * (mlt ((abs z1),(abs z2)))))) + (Sum (sqr (abs z2))) by RVSUM_1:89
.= ((Sum (sqr (abs z1))) + (Sum (2 * (mlt ((abs z1),(abs z2)))))) + (Sum (sqr (abs z2))) by RVSUM_1:89
.= ((Sum (sqr (abs z1))) + (2 * (Sum (mlt ((abs z1),(abs z2)))))) + (Sum (sqr (abs z2))) by RVSUM_1:87 ;
then Sum (sqr (abs (z1 + z2))) <= ((Sum (sqr (abs z1))) + (2 * (Sum (mlt ((abs z1),(abs z2)))))) + (Sum (sqr (abs z2))) by A9, RVSUM_1:82;
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 A8, 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 A2, A13, SQUARE_1:29;
then sqrt (Sum (sqr (abs (z1 + z2)))) <= sqrt (((sqrt (Sum (sqr (abs z1)))) + (sqrt (Sum (sqr (abs z2))))) ^2) by A15, A16, A1, SQUARE_1:26;
hence |.(z1 + z2).| <= |.z1.| + |.z2.| by A3, A14, SQUARE_1:22; :: thesis: verum