let a, b be Real_Sequence; :: thesis: for p being Real st 1 <= p & a rto_power p is summable & b rto_power p is summable holds
( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) )

let p be Real; :: thesis: ( 1 <= p & a rto_power p is summable & b rto_power p is summable implies ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) ) )
assume that
A1: 1 <= p and
A2: a rto_power p is summable and
A3: b rto_power p is summable ; :: thesis: ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) )
set ab = (a + b) rto_power p;
set bp = b rto_power p;
set ap = a rto_power p;
A4: now :: thesis: for n being Nat holds
( () . n = |.(a . n).| to_power p & () . n = |.(b . n).| to_power p & ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p )
let n be Nat; :: thesis: ( () . n = |.(a . n).| to_power p & () . n = |.(b . n).| to_power p & ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p )
thus (a rto_power p) . n = |.(a . n).| to_power p by Def1; :: thesis: ( () . n = |.(b . n).| to_power p & ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p )
thus (b rto_power p) . n = |.(b . n).| to_power p by Def1; :: thesis: ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p
((a + b) rto_power p) . n = |.((a + b) . n).| to_power p by Def1
.= |.((a . n) + (b . n)).| to_power p by SEQ_1:7 ;
hence ((a + b) rto_power p) . n = |.((a . n) + (b . n)).| to_power p ; :: thesis: verum
end;
reconsider p = p as Real ;
now :: thesis: ( ( p > 1 & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) & (a + b) rto_power p is summable ) or ( p = 1 & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) & (a + b) rto_power p is summable ) )
per cases ( p > 1 or p = 1 ) by ;
case p > 1 ; :: thesis: ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) & (a + b) rto_power p is summable )
hence ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) & (a + b) rto_power p is summable ) by ; :: thesis: verum
end;
case p = 1 ; :: thesis: ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) & (a + b) rto_power p is summable )
hence ( (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) & (a + b) rto_power p is summable ) by A2, A3, Lm4; :: thesis: verum
end;
end;
end;
hence ( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum ()) to_power (1 / p)) + ((Sum ()) to_power (1 / p)) ) ; :: thesis: verum