let N be Nat; :: thesis: for seq being Real_Sequence of N st seq is convergent & lim seq <> 0. (TOP-REAL N) holds
ex n being Nat st
for m being Nat st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
let seq be Real_Sequence of N; :: thesis: ( seq is convergent & lim seq <> 0. (TOP-REAL N) implies ex n being Nat st
for m being Nat st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).| )
assume that
A1: seq is convergent and
A2: lim seq <> 0. (TOP-REAL N) ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
0 <> |.(lim seq).| by A2, Th24;
then 0 < |.(lim seq).| / 2 by XREAL_1:215;
then consider n1 being Nat such that
A3: for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < |.(lim seq).| / 2 by A1, Def9;
take n = n1; :: thesis: for m being Nat st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
let m be Nat; :: thesis: ( n <= m implies |.(lim seq).| / 2 < |.(seq . m).| )
assume n <= m ; :: thesis: |.(lim seq).| / 2 < |.(seq . m).|
then A4: |.((seq . m) - (lim seq)).| < |.(lim seq).| / 2 by A3;
( |.(lim seq).| - |.(seq . m).| <= |.((lim seq) - (seq . m)).| & |.((lim seq) - (seq . m)).| = |.((seq . m) - (lim seq)).| ) by Th27, Th32;
then A5: |.(lim seq).| - |.(seq . m).| < |.(lim seq).| / 2 by A4, XXREAL_0:2;
( (|.(lim seq).| / 2) + (|.(seq . m).| - (|.(lim seq).| / 2)) = |.(seq . m).| & (|.(lim seq).| - |.(seq . m).|) + (|.(seq . m).| - (|.(lim seq).| / 2)) = |.(lim seq).| / 2 ) ;
hence |.(lim seq).| / 2 < |.(seq . m).| by A5, XREAL_1:6; :: thesis: verum