let seq be Complex_Sequence; :: 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 absolutely_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 absolutely_summable )
assume ( p > 1 & ( for n being Element of NAT st n >= 1 holds
|.seq.| . n = 1 / (n to_power p) ) ) ; :: thesis: seq is absolutely_summable
then |.seq.| is summable by SERIES_1:36;
hence seq is absolutely_summable by Def11; :: thesis: verum