let seq be Real_Sequence; :: thesis: ( ( seq is divergent_to+infty or seq is divergent_to-infty ) implies ( seq " is convergent & lim (seq ") = 0 ) )
assume A1: ( seq is divergent_to+infty or seq is divergent_to-infty ) ; :: thesis: ( seq " is convergent & lim (seq ") = 0 )
now :: thesis: ( seq " is convergent & seq " is convergent & lim (seq ") = 0 )
per cases ( seq is divergent_to+infty or seq is divergent_to-infty ) by A1;
suppose A2: seq is divergent_to+infty ; :: thesis: ( seq " is convergent & seq " is convergent & lim (seq ") = 0 )
A3: now :: thesis: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ") . m) - 0).| < r
let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ") . m) - 0).| < r )
assume A4: 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ") . m) - 0).| < r
consider n being Nat such that
A5: for m being Nat st n <= m holds
r " < seq . m by A2;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((seq ") . m) - 0).| < r
let m be Nat; :: thesis: ( n <= m implies |.(((seq ") . m) - 0).| < r )
assume n <= m ; :: thesis: |.(((seq ") . m) - 0).| < r
then A6: r " < seq . m by A5;
then 1 / (seq . m) < 1 / (r ") by A4, XREAL_1:76;
then A7: 1 / (seq . m) < r by XCMPLX_1:216;
A8: ( 1 / (seq . m) = (seq . m) " & (seq . m) " = (seq ") . m ) by VALUED_1:10, XCMPLX_1:215;
0 < r " by A4;
hence |.(((seq ") . m) - 0).| < r by A6, A7, A8, ABSVALUE:def 1; :: thesis: verum
end;
hence seq " is convergent ; :: thesis: ( seq " is convergent & lim (seq ") = 0 )
hence ( seq " is convergent & lim (seq ") = 0 ) by A3, SEQ_2:def 7; :: thesis: verum
end;
suppose A9: seq is divergent_to-infty ; :: thesis: ( seq " is convergent & seq " is convergent & lim (seq ") = 0 )
A10: now :: thesis: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ") . m) - 0).| < r
let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ") . m) - 0).| < r )
assume A11: 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ") . m) - 0).| < r
A12: - (r ") < - 0 by A11, XREAL_1:24;
consider n being Nat such that
A13: for m being Nat st n <= m holds
seq . m < - (r ") by A9;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((seq ") . m) - 0).| < r
let m be Nat; :: thesis: ( n <= m implies |.(((seq ") . m) - 0).| < r )
assume A14: n <= m ; :: thesis: |.(((seq ") . m) - 0).| < r
then seq . m < - (r ") by A13;
then 1 / (- (r ")) < 1 / (seq . m) by A12, XREAL_1:99;
then ((- 1) * (r ")) " < 1 / (seq . m) by XCMPLX_1:215;
then A15: ((- 1) ") * ((r ") ") < 1 / (seq . m) by XCMPLX_1:204;
seq . m < - 0 by A11, A13, A14;
then 1 / (seq . m) < 0 / (seq . m) by XREAL_1:75;
then |.(1 / (seq . m)).| = - (1 / (seq . m)) by ABSVALUE:def 1;
then - (1 * r) < - |.(1 / (seq . m)).| by A15;
then |.(1 / (seq . m)).| < r by XREAL_1:24;
then |.((seq . m) ").| < r by XCMPLX_1:215;
hence |.(((seq ") . m) - 0).| < r by VALUED_1:10; :: thesis: verum
end;
hence seq " is convergent ; :: thesis: ( seq " is convergent & lim (seq ") = 0 )
hence ( seq " is convergent & lim (seq ") = 0 ) by A10, SEQ_2:def 7; :: thesis: verum
end;
end;
end;
hence ( seq " is convergent & lim (seq ") = 0 ) ; :: thesis: verum