let seq be Real_Sequence; :: thesis: ( seq is convergent & 0 < lim seq implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(lim seq) / 2 < seq . m )
assume A1: ( seq is convergent & 0 < lim seq ) ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(lim seq) / 2 < seq . m
reconsider s1 = NAT --> ((lim seq) / 2) as Real_Sequence ;
s1 . 0 = (lim seq) / 2 by FUNCOP_1:13;
then B2: lim (seq - s1) = (((lim seq) / 2) + ((lim seq) / 2)) - ((lim seq) / 2) by A1, SEQ_4:59
.= (lim seq) / 2 ;
seq - s1 is convergent by A1, SEQ_2:25;
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
0 < (seq - s1) . m by B2, Th29, A1, XREAL_1:217;
take n ; :: 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 0 < (seq - s1) . m by A3;
then 0 < (seq . m) - (s1 . m) by RFUNCT_2:6;
then 0 < (seq . m) - ((lim seq) / 2) by FUNCOP_1:13;
then 0 + ((lim seq) / 2) < seq . m by XREAL_1:22;
hence (lim seq) / 2 < seq . m ; :: thesis: verum