let r be Real; :: thesis: for s being Real_Sequence st r > 0 & ex m being Nat st

for n being Nat st n >= m holds

|.(s . n).| >= r & s is convergent holds

lim s <> 0

let s be Real_Sequence; :: thesis: ( r > 0 & ex m being Nat st

for n being Nat st n >= m holds

|.(s . n).| >= r & s is convergent implies lim s <> 0 )

assume A1: r > 0 ; :: thesis: ( for m being Nat ex n being Nat st

( n >= m & not |.(s . n).| >= r ) or not s is convergent or lim s <> 0 )

given m being Nat such that A2: for n being Nat st n >= m holds

|.(s . n).| >= r ; :: thesis: ( not s is convergent or lim s <> 0 )

for n being Nat st n >= m holds

|.(s . n).| >= r & s is convergent holds

lim s <> 0

let s be Real_Sequence; :: thesis: ( r > 0 & ex m being Nat st

for n being Nat st n >= m holds

|.(s . n).| >= r & s is convergent implies lim s <> 0 )

assume A1: r > 0 ; :: thesis: ( for m being Nat ex n being Nat st

( n >= m & not |.(s . n).| >= r ) or not s is convergent or lim s <> 0 )

given m being Nat such that A2: for n being Nat st n >= m holds

|.(s . n).| >= r ; :: thesis: ( not s is convergent or lim s <> 0 )

now :: thesis: ( not s is convergent or lim s <> 0 )end;

hence
( not s is convergent or lim s <> 0 )
; :: thesis: verumper cases
( not s is convergent or s is convergent )
;

end;

suppose A3:
s is convergent
; :: thesis: ( not s is convergent or lim s <> 0 )

end;

now :: thesis: not lim s = 0

hence
( not s is convergent or lim s <> 0 )
; :: thesis: verumassume
lim s = 0
; :: thesis: contradiction

then consider k being Nat such that

A4: for n being Nat st n >= k holds

|.((s . n) - 0).| < r by A1, A3, SEQ_2:def 7;

end;then consider k being Nat such that

A4: for n being Nat st n >= k holds

|.((s . n) - 0).| < r by A1, A3, SEQ_2:def 7;

now :: thesis: for n being Nat holds not n >= m + k

hence
contradiction
; :: thesis: verumlet n be Nat; :: thesis: not n >= m + k

assume A5: n >= m + k ; :: thesis: contradiction

m + k >= k by NAT_1:11;

then n >= k by A5, XXREAL_0:2;

then A6: |.((s . n) - 0).| < r by A4;

m + k >= m by NAT_1:11;

then n >= m by A5, XXREAL_0:2;

hence contradiction by A2, A6; :: thesis: verum

end;assume A5: n >= m + k ; :: thesis: contradiction

m + k >= k by NAT_1:11;

then n >= k by A5, XXREAL_0:2;

then A6: |.((s . n) - 0).| < r by A4;

m + k >= m by NAT_1:11;

then n >= m by A5, XXREAL_0:2;

hence contradiction by A2, A6; :: thesis: verum