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