let N be Element of NAT ; :: thesis: for seq being Real_Sequence of N st seq is convergent & lim seq <> 0. (TOP-REAL N) holds
ex n being Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
0 <> |.(lim seq).| by A2, Th25;
then 0 < |.(lim seq).| / 2 by XREAL_1:217;
then consider n1 being Element of NAT such that
A3: for m being Element of NAT st n1 <= m holds
|.((seq . m) - (lim seq)).| < |.(lim seq).| / 2 by A1, Def10;
take n = n1; :: thesis: for m being Element of NAT st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
let m be Element of 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 Th28, Th33;
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:8; :: thesis: verum