let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n > 0 ) & ex m being Nat st

for n being Nat st n >= m holds

(s . (n + 1)) / (s . n) >= 1 implies not s is summable )

assume that

A1: for n being Nat holds s . n > 0 and

A2: ex m being Nat st

for n being Nat st n >= m holds

(s . (n + 1)) / (s . n) >= 1 ; :: thesis: not s is summable

consider m being Nat such that

A3: for n being Nat st n >= m holds

(s . (n + 1)) / (s . n) >= 1 by A2;

defpred S_{1}[ Nat] means s . (m + $1) >= s . m;

A4: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

A7: for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A6, A4);

A8: for k being Nat ex n being Nat st

( n >= k & not |.((s . n) - 0).| < s . m )

then ( not lim s = 0 or not s is convergent ) by A8, SEQ_2:def 7;

hence not s is summable by Th4; :: thesis: verum

for n being Nat st n >= m holds

(s . (n + 1)) / (s . n) >= 1 implies not s is summable )

assume that

A1: for n being Nat holds s . n > 0 and

A2: ex m being Nat st

for n being Nat st n >= m holds

(s . (n + 1)) / (s . n) >= 1 ; :: thesis: not s is summable

consider m being Nat such that

A3: for n being Nat st n >= m holds

(s . (n + 1)) / (s . n) >= 1 by A2;

defpred S

A4: for k being Nat st S

S

proof

A6:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: s . (m + k) >= s . m ; :: thesis: S_{1}[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:191;

hence S_{1}[k + 1]
by A5, XXREAL_0:2; :: thesis: verum

end;assume A5: s . (m + k) >= s . m ; :: thesis: S

( 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:191;

hence S

A7: for k being Nat holds S

A8: for k being Nat ex n being Nat st

( n >= k & not |.((s . n) - 0).| < s . m )

proof

s . m > 0
by A1;
let k be Nat; :: thesis: ex n being Nat st

( n >= k & not |.((s . n) - 0).| < s . m )

take n = m + k; :: thesis: ( n >= k & not |.((s . n) - 0).| < s . m )

s . n >= s . m by A7;

hence ( n >= k & not |.((s . n) - 0).| < s . m ) by NAT_1:11, SEQ_2:1; :: thesis: verum

end;( n >= k & not |.((s . n) - 0).| < s . m )

take n = m + k; :: thesis: ( n >= k & not |.((s . n) - 0).| < s . m )

s . n >= s . m by A7;

hence ( n >= k & not |.((s . n) - 0).| < s . m ) by NAT_1:11, SEQ_2:1; :: thesis: verum

then ( not lim s = 0 or not s is convergent ) by A8, SEQ_2:def 7;

hence not s is summable by Th4; :: thesis: verum