theorem :: COMSEQ_3:68

for seq being Complex_Sequence st ( for n being Nat holds |.seq.| . n > 0 ) & ex m being Nat st
for n being Nat st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 holds
not seq is absolutely_summable by SERIES_1:27;