let rseq1 be Real_Sequence; :: thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 holds
not |.seq.| is summable
let seq be Complex_Sequence; :: thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 implies not |.seq.| is summable )
assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 ) ; :: thesis: not |.seq.| is summable
for n being Element of NAT holds |.seq.| . n >= 0 by Lm3;
hence not |.seq.| is summable by A1, SERIES_1:29; :: thesis: verum