let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = 0 & ex k being Element of NAT st
for n being Element of 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 Element of NAT ex n being Element of NAT st
( k <= n & not 0 < seq . n ) or seq " is divergent_to+infty )
given k being Element of NAT such that A2: for n being Element of 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 Element of NAT st
for m being Element of NAT st n <= m holds
r < (seq " ) . m
set l = (abs r) + 1;
0 <= abs r by COMPLEX1:132;
then consider o being Element of NAT such that
A3: for n being Element of NAT st o <= n holds
abs ((seq . n) - 0 ) < ((abs r) + 1) " by A1, SEQ_2:def 7;
take m = max k,o; :: thesis: for m being Element of NAT st m <= m holds
r < (seq " ) . m
let n be Element of 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 abs ((seq . n) - 0 ) < ((abs r) + 1) " by A3;
then seq . n < ((abs r) + 1) " by A5, ABSVALUE:def 1;
then 1 / (((abs r) + 1) " ) < 1 / (seq . n) by A5, XREAL_1:78;
then A6: (abs r) + 1 < 1 / (seq . n) by XCMPLX_1:218;
r <= abs r by ABSVALUE:11;
then r < (abs r) + 1 by Lm1;
then r < 1 / (seq . n) by A6, XXREAL_0:2;
then r < (seq . n) " by XCMPLX_1:217;
hence r < (seq " ) . n by VALUED_1:10; :: thesis: verum