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 ;
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 = (() . \$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 ; :: thesis: verum
end;
suppose |.((a . n) + (b . n)).| > 0 ; :: thesis: 0 <= ab . n
hence 0 <= ab . n by ; :: 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 = (() . n) to_power (1 / p) by A6;
per cases ) . n = 0 or () . n > 0 ) by ;
suppose (Partial_Sums ab) . n = 0 ; :: thesis: 0 <= z . n
hence 0 <= z . n by ; :: thesis: verum
end;
suppose (Partial_Sums ab) . n > 0 ; :: thesis: 0 <= z . n
hence 0 <= z . n by ; :: thesis: verum
end;
end;
end;
A11: Partial_Sums ab is V48() by ;
A12: now :: thesis: for n, m being Nat st n <= m holds
(() . n) to_power (1 / p) <= (() . m) to_power (1 / p)
let n, m be Nat; :: thesis: ( n <= m implies (() . n) to_power (1 / p) <= (() . m) to_power (1 / p) )
assume n <= m ; :: thesis: (() . n) to_power (1 / p) <= (() . m) to_power (1 / p)
then A13: (Partial_Sums ab) . n <= () . m by ;
A14: 0 <= (() . m) to_power (1 / p)
proof
per cases ) . m = 0 or () . m > 0 ) by ;
suppose (Partial_Sums ab) . m = 0 ; :: thesis: 0 <= (() . m) to_power (1 / p)
hence 0 <= (() . m) to_power (1 / p) by ; :: thesis: verum
end;
suppose (Partial_Sums ab) . m > 0 ; :: thesis: 0 <= (() . m) to_power (1 / p)
hence 0 <= (() . m) to_power (1 / p) by POWER:34; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( () . n = () . m & (() . n) to_power (1 / p) <= (() . m) to_power (1 / p) ) or ( () . n <> () . m & (() . n) to_power (1 / p) <= (() . m) to_power (1 / p) ) )
per cases ) . n = () . m or () . n <> () . m ) ;
case (Partial_Sums ab) . n = () . m ; :: thesis: (() . n) to_power (1 / p) <= (() . m) to_power (1 / p)
hence ((Partial_Sums ab) . n) to_power (1 / p) <= (() . m) to_power (1 / p) ; :: thesis: verum
end;
case (Partial_Sums ab) . n <> () . m ; :: thesis: (() . n) to_power (1 / p) <= (() . m) to_power (1 / p)
then A15: (Partial_Sums ab) . n < () . m by ;
now :: thesis: ( ( () . n = 0 & (() . n) to_power (1 / p) <= (() . m) to_power (1 / p) ) or ( () . n <> 0 & (() . n) to_power (1 / p) <= (() . m) to_power (1 / p) ) )
per cases ) . n = 0 or () . n <> 0 ) ;
case (Partial_Sums ab) . n = 0 ; :: thesis: (() . n) to_power (1 / p) <= (() . m) to_power (1 / p)
hence ((Partial_Sums ab) . n) to_power (1 / p) <= (() . m) to_power (1 / p) by ; :: thesis: verum
end;
case A16: (Partial_Sums ab) . n <> 0 ; :: thesis: (() . n) to_power (1 / p) <= (() . m) to_power (1 / p)
0 <= () . n by ;
hence ((Partial_Sums ab) . n) to_power (1 / p) <= (() . m) to_power (1 / p) by ; :: thesis: verum
end;
end;
end;
hence ((Partial_Sums ab) . n) to_power (1 / p) <= (() . m) to_power (1 / p) ; :: thesis: verum
end;
end;
end;
hence ((Partial_Sums ab) . n) to_power (1 / p) <= (() . 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 = (() . n) to_power (1 / p) & z . m = (() . m) to_power (1 / p) ) by A6;
hence z . n <= z . m by ; :: thesis: verum
end;
then A18: z is V48() 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 ; :: thesis: verum
end;
case |.(a . n).| > 0 ; :: thesis: 0 <= ap . n
hence 0 <= ap . n by ; :: thesis: verum
end;
end;
end;
hence 0 <= ap . n ; :: thesis: verum
end;
then A20: for n being Nat holds 0 <= () . n by Lm2;
deffunc H2( Nat) -> object = (() . \$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 ; :: thesis: verum
end;
case |.(b . n).| > 0 ; :: thesis: 0 <= bp . n
hence 0 <= bp . n by ; :: thesis: verum
end;
end;
end;
hence 0 <= bp . n ; :: thesis: verum
end;
then A23: for n being Nat holds 0 <= () . n by Lm2;
deffunc H3( Nat) -> object = (() . \$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 ;
then A26: y is convergent by A2, A24, A23, Th10;
A27: Partial_Sums ap is convergent by ;
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 = (() . n) to_power (1 / p) by A24;
( ((Partial_Sums ab) . n) to_power (1 / p) <= ((() . n) to_power (1 / p)) + ((() . n) to_power (1 / p)) & x . n = (() . n) to_power (1 / p) ) by A1, A3, A21, Th7;
hence z . n <= (x . n) + (y . n) by ; :: thesis: verum
end;
then A31: z is convergent by A28, A26, A18, Th9;
A32: for n being Nat holds (z . n) to_power p = () . n
proof
let n be Nat; :: thesis: (z . n) to_power p = () . n
A33: z . n = (() . n) to_power (1 / p) by A6;
now :: thesis: ( ( () . n = 0 & (z . n) to_power p = () . n ) or ( () . n <> 0 & (z . n) to_power p = () . n ) )
per cases ) . n = 0 or () . n <> 0 ) ;
case A34: (Partial_Sums ab) . n = 0 ; :: thesis: (z . n) to_power p = () . n
then z . n = 0 by ;
hence (z . n) to_power p = () . n by ; :: thesis: verum
end;
case A35: (Partial_Sums ab) . n <> 0 ; :: thesis: (z . n) to_power p = () . n
0 <= () . n by ;
hence (z . n) to_power p = (() . n) to_power ((1 / p) * p) by
.= (() . n) to_power 1 by
.= () . n by POWER:25 ;
:: thesis: verum
end;
end;
end;
hence (z . n) to_power p = () . n ; :: thesis: verum
end;
then lim () = (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
.= lim z by ;
:: thesis: verum
end;
suppose lim z <> 0 ; :: thesis: (Sum ab) to_power (1 / p) = lim z
then 0 < lim z by ;
hence (Sum ab) to_power (1 / p) = (lim z) to_power ((1 / p) * p) by
.= (lim z) to_power 1 by
.= lim z by POWER:25 ;
:: thesis: verum
end;
end;
end;
Sum bp = lim () by SERIES_1:def 3;
then A39: lim y = (Sum bp) to_power (1 / p) by A2, A24, A25, A23, Th10;
Sum ap = lim () 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 ; :: thesis: verum