let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds s . n <> 0 ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
((abs s) . (n + 1)) / ((abs s) . n) >= 1 implies not s is summable )
assume A1: for n being Element of NAT holds s . n <> 0 ; :: thesis: ( for m being Element of NAT ex n being Element of NAT st
( n >= m & not ((abs s) . (n + 1)) / ((abs s) . n) >= 1 ) or not s is summable )
given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds
((abs s) . (n + 1)) / ((abs s) . n) >= 1 ; :: thesis: not s is summable
s . m <> 0 by A1;
then A3: abs (s . m) > 0 by COMPLEX1:133;

now

let n be Element of NAT ; :: thesis: ( n >= m implies abs (s . n) >= abs (s . m) )
assume A4: n >= m ; :: thesis: abs (s . n) >= abs (s . m)
defpred S₁[ Element of NAT ] means abs (s . (m + $1)) >= abs (s . m);
A5: S₁[ 0 ] ;
A6: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: abs (s . (m + k)) >= abs (s . m) ; :: thesis: S₁[k + 1]
((abs s) . ((m + k) + 1)) / ((abs s) . (m + k)) >= 1 by A2, NAT_1:11;
then (abs (s . ((m + k) + 1))) / ((abs s) . (m + k)) >= 1 by SEQ_1:16;
then A8: (abs (s . ((m + k) + 1))) / (abs (s . (m + k))) >= 1 by SEQ_1:16;
s . (m + k) <> 0 by A1;
then abs (s . (m + k)) > 0 by COMPLEX1:133;
then abs (s . ((m + k) + 1)) >= abs (s . (m + k)) by A8, XREAL_1:193;
hence S₁[k + 1] by A7, XXREAL_0:2; :: thesis: verum

end;

A9: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A5, A6);
consider k being Nat such that
A10: n = m + k by A4, NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
n = m + k by A10;
hence abs (s . n) >= abs (s . m) by A9; :: thesis: verum

end;

then ( not s is convergent or lim s <> 0 ) by A3, Th43;
hence not s is summable by Th7; :: thesis: verum