let s be convergent Complex_Sequence; :: thesis: ( lim s <> 0c implies ex n being Nat st
for m being Nat st n <= m holds
|.(lim s).| / 2 < |.(s . m).| )
assume A1: lim s <> 0c ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(lim s).| / 2 < |.(s . m).|
0 < |.(lim s).| by A1, COMPLEX1:47;
then 0 < |.(lim s).| / 2 ;
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
|.((s . m) - (lim s)).| < |.(lim s).| / 2 by Def6;
take n = n1; :: thesis: for m being Nat st n <= m holds
|.(lim s).| / 2 < |.(s . m).|
let m be Nat; :: thesis: ( n <= m implies |.(lim s).| / 2 < |.(s . m).| )
assume n <= m ; :: thesis: |.(lim s).| / 2 < |.(s . m).|
then A3: |.((s . m) - (lim s)).| < |.(lim s).| / 2 by A2;
A4: |.((lim s) - (s . m)).| = |.(- ((s . m) - (lim s))).|
.= |.((s . m) - (lim s)).| by COMPLEX1:52 ;
A5: ( (|.(lim s).| / 2) + (|.(s . m).| - (|.(lim s).| / 2)) = |.(s . m).| & (|.(lim s).| - |.(s . m).|) + (|.(s . m).| - (|.(lim s).| / 2)) = |.(lim s).| / 2 ) ;
|.(lim s).| - |.(s . m).| <= |.((lim s) - (s . m)).| by COMPLEX1:59;
then |.(lim s).| - |.(s . m).| < |.(lim s).| / 2 by A3, A4, XXREAL_0:2;
hence |.(lim s).| / 2 < |.(s . m).| by A5, XREAL_1:6; :: thesis: verum