let X be ComplexNormSpace; :: thesis: for seq being sequence of X
for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
seq is norm_summable
let seq be sequence of X; :: thesis: for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
seq is norm_summable
let p be Real; :: thesis: ( p > 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) implies seq is norm_summable )
assume ( p > 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) ) ; :: thesis: seq is norm_summable
then ||.seq.|| is summable by SERIES_1:32;
hence seq is norm_summable by Def4; :: thesis: verum