let rseq1 be Real_Sequence; :: thesis: for seq being Complex_Sequence st ( for n being Nat holds
( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is absolutely_summable
let seq be Complex_Sequence; :: thesis: ( ( for n being Nat holds
( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is absolutely_summable )
assume that
A1: for n being Nat holds
( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) and
A2: ( rseq1 is convergent & lim rseq1 < 1 ) ; :: thesis: seq is absolutely_summable
now :: thesis: for n being Nat holds
( |.seq.| . n <> 0 & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = (|.|.seq.|.| . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) )
let n be Nat; :: thesis: ( |.seq.| . n <> 0 & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = (|.|.seq.|.| . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) )
A3: ( seq . n <> 0c & |.seq.| . n = |.(seq . n).| ) by A1, VALUED_1:18;
hence ( |.seq.| . n <> 0 & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) by A1, COMPLEX1:47; :: thesis: ( |.seq.| . n <> 0 & rseq1 . n = (|.|.seq.|.| . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) )
thus ( |.seq.| . n <> 0 & rseq1 . n = (|.|.seq.|.| . (n + 1)) / (|.seq.| . n) ) by A1, A3, COMPLEX1:47; :: thesis: ( |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) )
thus ( |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) ) by A1, A3, COMPLEX1:47; :: thesis: verum
end;
then |.seq.| is absolutely_summable by A2, SERIES_1:37;
hence seq is absolutely_summable ; :: thesis: verum