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
seq . n < 0 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 seq . n < 0 ) 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
seq . n < 0 ; :: thesis: seq " is divergent_to-infty
let r be Real; :: according to LIMFUNC1:def 5 :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(seq " ) . m < r
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
(seq " ) . m < r
let n be Element of NAT ; :: thesis: ( m <= n implies (seq " ) . n < r )
assume A4: m <= n ; :: thesis: (seq " ) . n < r
k <= m by XXREAL_0:25;
then k <= n by A4, XXREAL_0:2;
then A5: seq . n < 0 by A2;
then A6: 0 < - (seq . n) by XREAL_1:60;
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 A6, XREAL_1:78;
then (abs r) + 1 < 1 / (- (seq . n)) by XCMPLX_1:218;
then (abs r) + 1 < (- (seq . n)) " by XCMPLX_1:217;
then (abs r) + 1 < - ((seq . n) " ) by XCMPLX_1:224;
then A7: - (- ((seq . n) " )) < - ((abs r) + 1) by XREAL_1:26;
- (abs r) <= r by ABSVALUE:11;
then (- (abs r)) - 1 < r by Lm1;
then (seq . n) " < r by A7, XXREAL_0:2;
hence (seq " ) . n < r by VALUED_1:10; :: thesis: verum