let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = 0 & ex k being Nat st
for n being Nat st k <= n holds
0 < seq . n implies seq " is divergent_to+infty )
assume A1: ( seq is convergent & lim seq = 0 ) ; :: thesis: ( for k being Nat ex n being Nat st
( k <= n & not 0 < seq . n ) or seq " is divergent_to+infty )
given k being Nat such that A2: for n being Nat st k <= n holds
0 < seq . n ; :: thesis: seq " is divergent_to+infty
let r be Real; :: according to LIMFUNC1:def 4 :: thesis: ex n being Nat st
for m being Nat st n <= m holds
r < (seq ") . m
set l = |.r.| + 1;
0 <= |.r.| by COMPLEX1:46;
then consider o being Nat such that
A3: for n being Nat st o <= n holds
|.((seq . n) - 0).| < (|.r.| + 1) " by A1, SEQ_2:def 7;
reconsider m = max (k,o) as Nat by TARSKI:1;
take m ; :: thesis: for m being Nat st m <= m holds
r < (seq ") . m
let n be Nat; :: thesis: ( m <= n implies r < (seq ") . n )
assume A4: m <= n ; :: thesis: r < (seq ") . n
k <= m by XXREAL_0:25;
then k <= n by A4, XXREAL_0:2;
then A5: 0 < seq . n by A2;
o <= m by XXREAL_0:25;
then o <= n by A4, XXREAL_0:2;
then |.((seq . n) - 0).| < (|.r.| + 1) " by A3;
then seq . n < (|.r.| + 1) " by A5, ABSVALUE:def 1;
then 1 / ((|.r.| + 1) ") < 1 / (seq . n) by A5, XREAL_1:76;
then A6: |.r.| + 1 < 1 / (seq . n) by XCMPLX_1:216;
r <= |.r.| by ABSVALUE:4;
then r < |.r.| + 1 by Lm1;
then r < 1 / (seq . n) by A6, XXREAL_0:2;
then r < (seq . n) " by XCMPLX_1:215;
hence r < (seq ") . n by VALUED_1:10; :: thesis: verum