let seq be Complex_Sequence; :: thesis: ( ( for n being Nat holds seq . n <> 0c ) & ex m being Nat st
for n being Nat st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 implies not seq is absolutely_summable )
assume that
A1: for n being Nat holds seq . n <> 0c and
A2: ex m being Nat st
for n being Nat st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 ; :: thesis: not seq is absolutely_summable
consider m being Nat such that
A3: for n being Nat st n >= m holds
(|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 by A2;
A4: now :: thesis: for n being Nat holds |.seq.| . n <> 0
let n be Nat; :: thesis: |.seq.| . n <> 0
seq . n <> 0c by A1;
then |.(seq . n).| <> 0 by COMPLEX1:47;
hence |.seq.| . n <> 0 by VALUED_1:18; :: thesis: verum
end;
for n being Nat st n >= m holds
((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) >= 1 by A3;
hence not |.seq.| is summable by A4, SERIES_1:39; :: according to COMSEQ_3:def 9 :: thesis: verum