let s, s1 be Real_Sequence; :: thesis: ( ( for n being Nat holds
( s . n <> 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) ) & s1 is convergent & lim s1 < 1 implies s is absolutely_summable )
assume that
A1: for n being Nat holds
( s . n <> 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) and
A2: ( s1 is convergent & lim s1 < 1 ) ; :: thesis: s is absolutely_summable
now :: thesis: for n being Nat holds
( (abs s) . n > 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) )
let n be Nat; :: thesis: ( (abs s) . n > 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) )
( (abs s) . n = |.(s . n).| & s . n <> 0 ) by A1, SEQ_1:12;
hence (abs s) . n > 0 by COMPLEX1:47; :: thesis: s1 . n = ((abs s) . (n + 1)) / ((abs s) . n)
thus s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) by A1; :: thesis: verum
end;
then abs s is summable by A2, Th26;
hence s is absolutely_summable ; :: thesis: verum