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 that
A1: seq is convergent and
A2: 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 ;
A3: seq - s1 is convergent by A1;
s1 . 0 = (lim seq) / 2 by FUNCOP_1:7;
then lim (seq - s1) = (((lim seq) / 2) + ((lim seq) / 2)) - ((lim seq) / 2) by A1, SEQ_4:42
.= (lim seq) / 2 ;
then consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
0 < (seq - s1) . m by A2, A3, Th29, XREAL_1:215;
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 A4;
then 0 < (seq . m) - (s1 . m) by RFUNCT_2:1;
then 0 < (seq . m) - ((lim seq) / 2) by FUNCOP_1:7;
then 0 + ((lim seq) / 2) < seq . m by XREAL_1:20;
hence (lim seq) / 2 < seq . m ; :: thesis: verum