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 A1: ( ( 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 ) ; :: thesis: not seq is absolutely_summable

A2: 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;

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 A1;
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 A2, SERIES_1:44; :: according to COMSEQ_3:def 11 :: thesis: verum