let seq be Complex_Sequence; :: thesis: ( ( for n being Element of NAT holds seq . n <> 0c ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 implies not seq is absolutely_summable )
assume that
A1: for n being Element of NAT holds seq . n <> 0c and
A2: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 ; :: thesis: not seq is absolutely_summable
consider m being Element of NAT such that
A3: for n being Element of NAT st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 by A2;

A4: now

let n be Element of NAT ; :: thesis: |.seq.| . n <> 0
seq . n <> 0c by A1;
then |.(seq . n).| <> 0 by COMPLEX1:133;
hence |.seq.| . n <> 0 by VALUED_1:18; :: thesis: verum

end;

for n being Element of NAT st n >= m holds
((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) >= 1 by A3;
hence not |.seq.| is summable by A4, SERIES_1:44; :: according to COMSEQ_3:def 13 :: thesis: verum