let s be Complex_Sequence; :: thesis: ( s is convergent & lim s <> 0c implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim s).| / 2 < |.(s . m).| )
assume that
A1: s is convergent and
A2: lim s <> 0c ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim s).| / 2 < |.(s . m).|
0 < |.(lim s).| by A2, COMPLEX1:133;
then 0 < |.(lim s).| / 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
|.((s . m) - (lim s)).| < |.(lim s).| / 2 by A1, Def5;
take n = n1; :: thesis: for m being Element of NAT st n <= m holds
|.(lim s).| / 2 < |.(s . m).|
let m be Element of NAT ; :: thesis: ( n <= m implies |.(lim s).| / 2 < |.(s . m).| )
assume n <= m ; :: thesis: |.(lim s).| / 2 < |.(s . m).|
then A4: |.((s . m) - (lim s)).| < |.(lim s).| / 2 by A3;
A5: |.(lim s).| - |.(s . m).| <= |.((lim s) - (s . m)).| by COMPLEX1:145;
|.((lim s) - (s . m)).| = |.(- ((s . m) - (lim s))).|
.= |.((s . m) - (lim s)).| by COMPLEX1:138 ;
then A6: |.(lim s).| - |.(s . m).| < |.(lim s).| / 2 by A4, A5, XXREAL_0:2;
A7: (|.(lim s).| / 2) + (|.(s . m).| - (|.(lim s).| / 2)) = |.(s . m).| ;
(|.(lim s).| - |.(s . m).|) + (|.(s . m).| - (|.(lim s).| / 2)) = |.(lim s).| / 2 ;
hence |.(lim s).| / 2 < |.(s . m).| by A6, A7, XREAL_1:8; :: thesis: verum