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
(s . (n + 1)) / (s . n) >= 1 implies not s is summable )
assume that
A1: for n being Element of NAT holds s . n > 0 and
A2: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(s . (n + 1)) / (s . n) >= 1 ; :: thesis: not s is summable
consider m being Element of NAT such that
A3: for n being Element of NAT st n >= m holds
(s . (n + 1)) / (s . n) >= 1 by A2;
defpred S₁[ Element of NAT ] means s . (m + $1) >= s . m;
A4: 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 A5: s . (m + k) >= s . m ; :: thesis: S₁[k + 1]
( s . (m + k) > 0 & (s . ((m + k) + 1)) / (s . (m + k)) >= 1 ) by A1, A3, NAT_1:11;
then s . ((m + k) + 1) >= s . (m + k) by XREAL_1:193;
hence S₁[k + 1] by A5, XXREAL_0:2; :: thesis: verum

end;

A6: S₁[ 0 ] ;
A7: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A6, A4);
A8: for k being Element of NAT ex n being Element of NAT st
( n >= k & not abs ((s . n) - 0 ) < s . m )

proof

let k be Element of NAT ; :: thesis: ex n being Element of NAT st
( n >= k & not abs ((s . n) - 0 ) < s . m )
take n = m + k; :: thesis: ( n >= k & not abs ((s . n) - 0 ) < s . m )
s . n >= s . m by A7;
hence ( n >= k & not abs ((s . n) - 0 ) < s . m ) by NAT_1:11, SEQ_2:9; :: thesis: verum

end;

s . m > 0 by A1;
then ( not lim s = 0 or not s is convergent ) by A8, SEQ_2:def 7;
hence not s is summable by Th7; :: thesis: verum