let rseq1 be Real_Sequence; :: thesis: for seq being Complex_Sequence st |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) holds
( seq is absolutely_summable iff rseq1 is summable )
let seq be Complex_Sequence; :: thesis: ( |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) implies ( seq is absolutely_summable iff rseq1 is summable ) )
assume ( |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) ) ; :: thesis: ( seq is absolutely_summable iff rseq1 is summable )
then for n being Element of NAT holds
( |.seq.| is non-increasing & |.seq.| . n >= 0 & rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) by Lm3;
then ( |.seq.| is summable iff rseq1 is summable ) by SERIES_1:31;
hence ( seq is absolutely_summable iff rseq1 is summable ) by Def13; :: thesis: verum