let X be ComplexNormSpace; :: thesis: for seq being sequence of X st ( for n being Nat holds seq . n <> 0. X ) & ex m being Nat st
for n being Nat st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 holds
not seq is norm_summable
let seq be sequence of X; :: thesis: ( ( for n being Nat holds seq . n <> 0. X ) & ex m being Nat st
for n being Nat st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 implies not seq is norm_summable )
assume that
A1: for n being Nat holds seq . n <> 0. X 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 norm_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 st n >= m holds
((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1

let n be Nat; :: thesis: ( n >= m implies ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 )
assume A5: n >= m ; :: thesis: ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1
A6: 0 <= ||.seq.|| . n by Th2;
A7: 0 <= ||.seq.|| . (n + 1) by Th2;
A8: (abs ||.seq.||) . (n + 1) = |.(||.seq.|| . (n + 1)).| by SEQ_1:12
.= ||.seq.|| . (n + 1) by A7, ABSVALUE:def 1 ;
(abs ||.seq.||) . n = |.(||.seq.|| . n).| by SEQ_1:12
.= ||.seq.|| . n by A6, ABSVALUE:def 1 ;
hence ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 by A3, A5, A8; :: thesis: verum

end;

now :: thesis: for n being Nat holds ||.seq.|| . n <> 0

let n be Nat; :: thesis: ||.seq.|| . n <> 0
seq . n <> 0. X by A1;
then ||.(seq . n).|| <> 0 by NORMSP_0:def 5;
hence ||.seq.|| . n <> 0 by NORMSP_0:def 4; :: thesis: verum

end;

hence not ||.seq.|| is summable by A4, SERIES_1:39; :: according to CLOPBAN3:def 3 :: thesis: verum