let p be Real; :: thesis: ( 1 < p implies for a, b, ap, bp, ab being Real_Sequence st ( for n being Nat holds
( ap . n = |.(a . n).| to_power p & bp . n = |.(b . n).| to_power p & ab . n = |.((a . n) + (b . n)).| to_power p ) ) & ap is summable & bp is summable holds
( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) ) )
assume A1: 1 < p ; :: thesis: for a, b, ap, bp, ab being Real_Sequence st ( for n being Nat holds
( ap . n = |.(a . n).| to_power p & bp . n = |.(b . n).| to_power p & ab . n = |.((a . n) + (b . n)).| to_power p ) ) & ap is summable & bp is summable holds
( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) )
A2: 1 / p > 0 by A1, XREAL_1:139;
let a, b, ap, bp, ab be Real_Sequence; :: thesis: ( ( for n being Nat holds
( ap . n = |.(a . n).| to_power p & bp . n = |.(b . n).| to_power p & ab . n = |.((a . n) + (b . n)).| to_power p ) ) & ap is summable & bp is summable implies ( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) ) )
assume that
A3: for n being Nat holds
( ap . n = |.(a . n).| to_power p & bp . n = |.(b . n).| to_power p & ab . n = |.((a . n) + (b . n)).| to_power p ) and
A4: ap is summable and
A5: bp is summable ; :: thesis: ( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) )
deffunc H1( Nat) -> object = ((Partial_Sums ab) . $1) to_power (1 / p);
consider z being Real_Sequence such that
A6: for n being Nat holds z . n = H1(n) from SEQ_1:sch 1();
 A7: for n being Nat holds 0 <= ab . n
proof
let n be Nat; :: thesis: 0 <= ab . n
A8: ab . n = |.((a . n) + (b . n)).| to_power p by A3;
per cases ( |.((a . n) + (b . n)).| = 0 or |.((a . n) + (b . n)).| > 0 ) by COMPLEX1:46;
suppose |.((a . n) + (b . n)).| = 0 ; :: thesis: 0 <= ab . n
hence 0 <= ab . n by A1, A8, POWER:def 2; :: thesis: verum
end;
suppose |.((a . n) + (b . n)).| > 0 ; :: thesis: 0 <= ab . n
hence 0 <= ab . n by A8, POWER:34; :: thesis: verum
end;
end;
end;
A9: for n being Nat holds 0 <= z . n
proof
let n be Nat; :: thesis: 0 <= z . n
A10: z . n = ((Partial_Sums ab) . n) to_power (1 / p) by A6;
per cases ( (Partial_Sums ab) . n = 0 or (Partial_Sums ab) . n > 0 ) by A7, Lm2;
suppose (Partial_Sums ab) . n > 0 ; :: thesis: 0 <= z . n
hence 0 <= z . n by A10, POWER:34; :: thesis: verum
end;
end;
end;
A11: Partial_Sums ab is non-decreasing by A7, SERIES_1:16;
A12: now :: thesis: for n, m being Nat st n <= m holds
((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p)
let n, m be Nat; :: thesis: ( n <= m implies ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) )
assume n <= m ; :: thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p)
then A13: (Partial_Sums ab) . n <= (Partial_Sums ab) . m by A11, SEQM_3:6;
A14: 0 <= ((Partial_Sums ab) . m) to_power (1 / p)
proof
per cases ( (Partial_Sums ab) . m = 0 or (Partial_Sums ab) . m > 0 ) by A7, Lm2;
suppose (Partial_Sums ab) . m > 0 ; :: thesis: 0 <= ((Partial_Sums ab) . m) to_power (1 / p)
hence 0 <= ((Partial_Sums ab) . m) to_power (1 / p) by POWER:34; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( (Partial_Sums ab) . n = (Partial_Sums ab) . m & ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ) or ( (Partial_Sums ab) . n <> (Partial_Sums ab) . m & ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ) )
per cases ( (Partial_Sums ab) . n = (Partial_Sums ab) . m or (Partial_Sums ab) . n <> (Partial_Sums ab) . m ) ;
case (Partial_Sums ab) . n = (Partial_Sums ab) . m ; :: thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p)
hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ; :: thesis: verum
end;
case (Partial_Sums ab) . n <> (Partial_Sums ab) . m ; :: thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p)
then A15: (Partial_Sums ab) . n < (Partial_Sums ab) . m by A13, XXREAL_0:1;
now :: thesis: ( ( (Partial_Sums ab) . n = 0 & ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ) or ( (Partial_Sums ab) . n <> 0 & ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ) )
per cases ( (Partial_Sums ab) . n = 0 or (Partial_Sums ab) . n <> 0 ) ;
case (Partial_Sums ab) . n = 0 ; :: thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p)
hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) by A2, A14, POWER:def 2; :: thesis: verum
end;
case A16: (Partial_Sums ab) . n <> 0 ; :: thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p)
0 <= (Partial_Sums ab) . n by A7, Lm2;
hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) by A2, A15, A16, POWER:37; :: thesis: verum
end;
end;
end;
hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ; :: thesis: verum
end;
end;
end;
hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ; :: thesis: verum
end;
now :: thesis: for n, m being Nat st n <= m holds
z . n <= z . m
let n, m be Nat; :: thesis: ( n <= m implies z . n <= z . m )
assume A17: n <= m ; :: thesis: z . n <= z . m
( z . n = ((Partial_Sums ab) . n) to_power (1 / p) & z . m = ((Partial_Sums ab) . m) to_power (1 / p) ) by A6;
hence z . n <= z . m by A12, A17; :: thesis: verum
end;
then A18: z is non-decreasing by SEQM_3:6;
for n being Nat holds 0 <= ap . n
proof
let n be Nat; :: thesis: 0 <= ap . n
A19: ap . n = |.(a . n).| to_power p by A3;
now :: thesis: ( ( |.(a . n).| = 0 & 0 <= ap . n ) or ( |.(a . n).| > 0 & 0 <= ap . n ) )
per cases ( |.(a . n).| = 0 or |.(a . n).| > 0 ) by COMPLEX1:46;
case |.(a . n).| = 0 ; :: thesis: 0 <= ap . n
hence 0 <= ap . n by A1, A19, POWER:def 2; :: thesis: verum
end;
case |.(a . n).| > 0 ; :: thesis: 0 <= ap . n
hence 0 <= ap . n by A19, POWER:34; :: thesis: verum
end;
end;
end;
hence 0 <= ap . n ; :: thesis: verum
end;
then A20: for n being Nat holds 0 <= (Partial_Sums ap) . n by Lm2;
deffunc H2( Nat) -> object = ((Partial_Sums ap) . $1) to_power (1 / p);
consider x being Real_Sequence such that
A21: for n being Nat holds x . n = H2(n) from SEQ_1:sch 1();
 for n being Nat holds 0 <= bp . n
proof
let n be Nat; :: thesis: 0 <= bp . n
A22: bp . n = |.(b . n).| to_power p by A3;
now :: thesis: ( ( |.(b . n).| = 0 & 0 <= bp . n ) or ( |.(b . n).| > 0 & 0 <= bp . n ) )
per cases ( |.(b . n).| = 0 or |.(b . n).| > 0 ) by COMPLEX1:46;
case |.(b . n).| = 0 ; :: thesis: 0 <= bp . n
hence 0 <= bp . n by A1, A22, POWER:def 2; :: thesis: verum
end;
case |.(b . n).| > 0 ; :: thesis: 0 <= bp . n
hence 0 <= bp . n by A22, POWER:34; :: thesis: verum
end;
end;
end;
hence 0 <= bp . n ; :: thesis: verum
end;
then A23: for n being Nat holds 0 <= (Partial_Sums bp) . n by Lm2;
deffunc H3( Nat) -> object = ((Partial_Sums bp) . $1) to_power (1 / p);
consider y being Real_Sequence such that
A24: for n being Nat holds y . n = H3(n) from SEQ_1:sch 1();
 A25: Partial_Sums bp is convergent by A5, SERIES_1:def 2;
then A26: y is convergent by A2, A24, A23, Th10;
A27: Partial_Sums ap is convergent by A4, SERIES_1:def 2;
then A28: x is convergent by A2, A21, A20, Th10;
A29: for n being Nat holds z . n <= (x . n) + (y . n)
proof
let n be Nat; :: thesis: z . n <= (x . n) + (y . n)
A30: y . n = ((Partial_Sums bp) . n) to_power (1 / p) by A24;
( ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) & x . n = ((Partial_Sums ap) . n) to_power (1 / p) ) by A1, A3, A21, Th7;
hence z . n <= (x . n) + (y . n) by A6, A30; :: thesis: verum
end;
then A31: z is convergent by A28, A26, A18, Th9;
A32: for n being Nat holds (z . n) to_power p = (Partial_Sums ab) . n
proof
let n be Nat; :: thesis: (z . n) to_power p = (Partial_Sums ab) . n
A33: z . n = ((Partial_Sums ab) . n) to_power (1 / p) by A6;
now :: thesis: ( ( (Partial_Sums ab) . n = 0 & (z . n) to_power p = (Partial_Sums ab) . n ) or ( (Partial_Sums ab) . n <> 0 & (z . n) to_power p = (Partial_Sums ab) . n ) )
per cases ( (Partial_Sums ab) . n = 0 or (Partial_Sums ab) . n <> 0 ) ;
case A35: (Partial_Sums ab) . n <> 0 ; :: thesis: (z . n) to_power p = (Partial_Sums ab) . n
0 <= (Partial_Sums ab) . n by A7, Lm2;
hence (z . n) to_power p = ((Partial_Sums ab) . n) to_power ((1 / p) * p) by A33, A35, POWER:33
.= ((Partial_Sums ab) . n) to_power 1 by A1, XCMPLX_1:106
.= (Partial_Sums ab) . n by POWER:25 ;
:: thesis: verum
end;
end;
end;
hence (z . n) to_power p = (Partial_Sums ab) . n ; :: thesis: verum
end;
then lim (Partial_Sums ab) = (lim z) to_power p by A1, A9, A31, Th10;
then A36: Sum ab = (lim z) to_power p by SERIES_1:def 3;
A37: (Sum ab) to_power (1 / p) = lim z
proof
per cases ( lim z = 0 or lim z <> 0 ) ;
suppose A38: lim z = 0 ; :: thesis: (Sum ab) to_power (1 / p) = lim z
hence (Sum ab) to_power (1 / p) = 0 to_power (1 / p) by A1, A36, POWER:def 2
.= lim z by A2, A38, POWER:def 2 ;
:: thesis: verum
end;
suppose lim z <> 0 ; :: thesis: (Sum ab) to_power (1 / p) = lim z
then 0 < lim z by A9, A31, SEQ_2:17;
hence (Sum ab) to_power (1 / p) = (lim z) to_power ((1 / p) * p) by A36, POWER:33
.= (lim z) to_power 1 by A1, XCMPLX_1:106
.= lim z by POWER:25 ;
:: thesis: verum
end;
end;
end;
Sum bp = lim (Partial_Sums bp) by SERIES_1:def 3;
then A39: lim y = (Sum bp) to_power (1 / p) by A2, A24, A25, A23, Th10;
Sum ap = lim (Partial_Sums ap) by SERIES_1:def 3;
then A40: lim x = (Sum ap) to_power (1 / p) by A2, A21, A27, A20, Th10;
Partial_Sums ab is convergent by A1, A9, A31, A32, Th10;
hence ( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) ) by A28, A40, A26, A39, A29, A18, A37, Th9, SERIES_1:def 2; :: thesis: verum