let p be Real; :: thesis: ( 1 < p implies for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds
( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((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 Element of NAT holds
( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((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:141;
let a, b, ap, bp, ab be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds
( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((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 Element of NAT holds
( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((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( Element of NAT ) -> Element of REAL = ((Partial_Sums ap) . $1) to_power (1 / p);
consider x being Real_Sequence such that
A6: for n being Element of NAT holds x . n = H1(n) from SEQ_1:sch 1();
 deffunc H2( Element of NAT ) -> Element of REAL = ((Partial_Sums bp) . $1) to_power (1 / p);
consider y being Real_Sequence such that
A7: for n being Element of NAT holds y . n = H2(n) from SEQ_1:sch 1();
 A8: Partial_Sums ap is convergent by A4, SERIES_1:def 2;
A9: Sum ap = lim (Partial_Sums ap) by SERIES_1:def 3;
for n being Element of NAT holds 0 <= ap . n
proof
let n be Element of NAT ; :: thesis: 0 <= ap . n
A10: ap . n = (abs (a . n)) to_power p by A3;
now
per cases ( abs (a . n) = 0 or abs (a . n) > 0 ) by COMPLEX1:132;
case abs (a . n) = 0 ; :: thesis: 0 <= ap . n
hence 0 <= ap . n by A1, A10, POWER:def 2; :: thesis: verum
end;
case abs (a . n) > 0 ; :: thesis: 0 <= ap . n
hence 0 <= ap . n by A10, POWER:39; :: thesis: verum
end;
end;
end;
hence 0 <= ap . n ; :: thesis: verum
end;
then for n being Element of NAT holds 0 <= (Partial_Sums ap) . n by Lm2;
then A11: ( x is convergent & lim x = (Sum ap) to_power (1 / p) ) by A2, A6, A8, A9, Th10;
A12: Partial_Sums bp is convergent by A5, SERIES_1:def 2;
A13: Sum bp = lim (Partial_Sums bp) by SERIES_1:def 3;
for n being Element of NAT holds 0 <= bp . n
proof
let n be Element of NAT ; :: thesis: 0 <= bp . n
A14: bp . n = (abs (b . n)) to_power p by A3;
now
per cases ( abs (b . n) = 0 or abs (b . n) > 0 ) by COMPLEX1:132;
case abs (b . n) = 0 ; :: thesis: 0 <= bp . n
hence 0 <= bp . n by A1, A14, POWER:def 2; :: thesis: verum
end;
case abs (b . n) > 0 ; :: thesis: 0 <= bp . n
hence 0 <= bp . n by A14, POWER:39; :: thesis: verum
end;
end;
end;
hence 0 <= bp . n ; :: thesis: verum
end;
then for n being Element of NAT holds 0 <= (Partial_Sums bp) . n by Lm2;
then A15: ( y is convergent & lim y = (Sum bp) to_power (1 / p) ) by A2, A7, A12, A13, Th10;
deffunc H3( Element of NAT ) -> Element of REAL = ((Partial_Sums ab) . $1) to_power (1 / p);
consider z being Real_Sequence such that
A16: for n being Element of NAT holds z . n = H3(n) from SEQ_1:sch 1();
 A17: for n being Element of NAT holds z . n <= (x . n) + (y . n)
proof
let n be Element of NAT ; :: thesis: z . n <= (x . n) + (y . n)
A18: ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) by A1, A3, Th7;
A19: x . n = ((Partial_Sums ap) . n) to_power (1 / p) by A6;
y . n = ((Partial_Sums bp) . n) to_power (1 / p) by A7;
hence z . n <= (x . n) + (y . n) by A16, A18, A19; :: thesis: verum
end;
A20: for n being Element of NAT holds 0 <= ab . n
proof
let n be Element of NAT ; :: thesis: 0 <= ab . n
A21: ab . n = (abs ((a . n) + (b . n))) to_power p by A3;
per cases ( abs ((a . n) + (b . n)) = 0 or abs ((a . n) + (b . n)) > 0 ) by COMPLEX1:132;
suppose abs ((a . n) + (b . n)) = 0 ; :: thesis: 0 <= ab . n
hence 0 <= ab . n by A1, A21, POWER:def 2; :: thesis: verum
end;
suppose abs ((a . n) + (b . n)) > 0 ; :: thesis: 0 <= ab . n
hence 0 <= ab . n by A21, POWER:39; :: thesis: verum
end;
end;
end;
A22: for n being Element of NAT holds 0 <= z . n
proof
let n be Element of NAT ; :: thesis: 0 <= z . n
A23: z . n = ((Partial_Sums ab) . n) to_power (1 / p) by A16;
per cases ( (Partial_Sums ab) . n = 0 or (Partial_Sums ab) . n > 0 ) by A20, Lm2;
suppose (Partial_Sums ab) . n > 0 ; :: thesis: 0 <= z . n
hence 0 <= z . n by A23, POWER:39; :: thesis: verum
end;
end;
end;
A24: z is non-decreasing
proof
A25: Partial_Sums ab is non-decreasing by A20, SERIES_1:19;
A26: now
let n, m be Element of NAT ; :: thesis: ( n <= m implies ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) )
assume A27: n <= m ; :: thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p)
A28: (Partial_Sums ab) . n <= (Partial_Sums ab) . m by A25, A27, SEQM_3:12;
A29: 0 <= ((Partial_Sums ab) . m) to_power (1 / p)
proof
per cases ( (Partial_Sums ab) . m = 0 or (Partial_Sums ab) . m > 0 ) by A20, 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:39; :: thesis: verum
end;
end;
end;
now
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 A30: (Partial_Sums ab) . n < (Partial_Sums ab) . m by A28, XXREAL_0:1;
now
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, A29, POWER:def 2; :: thesis: verum
end;
case A31: (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 A20, Lm2;
hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) by A2, A30, A31, POWER:42; :: 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
let n, m be Element of NAT ; :: thesis: ( n <= m implies z . n <= z . m )
assume A32: n <= m ; :: thesis: z . n <= z . m
A33: z . n = ((Partial_Sums ab) . n) to_power (1 / p) by A16;
z . m = ((Partial_Sums ab) . m) to_power (1 / p) by A16;
hence z . n <= z . m by A26, A32, A33; :: thesis: verum
end;
hence z is non-decreasing by SEQM_3:12; :: thesis: verum
end;
then A34: ( z is convergent & lim z <= (lim x) + (lim y) ) by A11, A15, A17, Th9;
for n being Element of NAT holds (z . n) to_power p = (Partial_Sums ab) . n
proof
let n be Element of NAT ; :: thesis: (z . n) to_power p = (Partial_Sums ab) . n
A35: z . n = ((Partial_Sums ab) . n) to_power (1 / p) by A16;
now
per cases ( (Partial_Sums ab) . n = 0 or (Partial_Sums ab) . n <> 0 ) ;
case A37: (Partial_Sums ab) . n <> 0 ; :: thesis: (z . n) to_power p = (Partial_Sums ab) . n
0 <= (Partial_Sums ab) . n by A20, Lm2;
hence (z . n) to_power p = ((Partial_Sums ab) . n) to_power ((1 / p) * p) by A35, A37, POWER:38
.= ((Partial_Sums ab) . n) to_power 1 by A1, XCMPLX_1:107
.= (Partial_Sums ab) . n by POWER:30 ;
:: thesis: verum
end;
end;
end;
hence (z . n) to_power p = (Partial_Sums ab) . n ; :: thesis: verum
end;
then A38: ( Partial_Sums ab is convergent & lim (Partial_Sums ab) = (lim z) to_power p ) by A1, A22, A34, Th10;
then A39: ( ab is summable & Sum ab = (lim z) to_power p ) by SERIES_1:def 2, SERIES_1:def 3;
(Sum ab) to_power (1 / p) = lim z
proof
per cases ( lim z = 0 or lim z <> 0 ) ;
suppose A40: 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, A39, POWER:def 2
.= lim z by A2, A40, POWER:def 2 ;
:: thesis: verum
end;
suppose lim z <> 0 ; :: thesis: (Sum ab) to_power (1 / p) = lim z
then 0 < lim z by A22, A34, SEQ_2:31;
hence (Sum ab) to_power (1 / p) = (lim z) to_power ((1 / p) * p) by A39, POWER:38
.= (lim z) to_power 1 by A1, XCMPLX_1:107
.= lim z by POWER:30 ;
:: thesis: verum
end;
end;
end;
hence ( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) ) by A11, A15, A17, A24, A38, Th9, SERIES_1:def 2; :: thesis: verum