theorem :: COMSEQ_3:71

for rseq1 being Real_Sequence
for seq being Complex_Sequence st ( for n being Nat holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds
not seq is absolutely_summable