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
seq . n < 0 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 seq . n < 0 ) or seq " is divergent_to-infty )
given k being Nat such that A2: for n being 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 Nat st
for m being Nat st n <= m holds
(seq ") . m < r
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
(seq ") . m < r
let n be 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:58;
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 A6, XREAL_1:76;
then |.r.| + 1 < 1 / (- (seq . n)) by XCMPLX_1:216;
then |.r.| + 1 < (- (seq . n)) " by XCMPLX_1:215;
then |.r.| + 1 < - ((seq . n) ") by XCMPLX_1:222;
then A7: - (- ((seq . n) ")) < - (|.r.| + 1) by XREAL_1:24;
- |.r.| <= r by ABSVALUE:4;
then (- |.r.|) - 1 < r by Lm1;
then (seq . n) " < r by A7, XXREAL_0:2;
hence (seq ") . n < r by VALUED_1:10; :: thesis: verum