let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq <> 0 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 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
0 < |.(lim seq).| by A2, COMPLEX1:47;
then 0 < |.(lim seq).| / 2 ;
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, Def6;
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;
A5: |.(lim seq).| - |.(seq . m).| <= |.((lim seq) - (seq . m)).| by COMPLEX1:59;
|.((lim seq) - (seq . m)).| = |.(- ((seq . m) - (lim seq))).|
.= |.((seq . m) - (lim seq)).| by COMPLEX1:52 ;
then A6: |.(lim seq).| - |.(seq . m).| < |.(lim seq).| / 2 by A4, A5, XXREAL_0:2;
A7: (|.(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 A6, A7, XREAL_1:6; :: thesis: verum