let seq be Real_Sequence; :: thesis: ( seq is convergent & 0 < lim seq implies ex n being Nat st
for m being 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 Nat st
for m being Nat st n <= m holds
(lim seq) / 2 < seq . m
reconsider ls = (lim seq) / 2 as Element of REAL by XREAL_0:def 1;
set s1 = seq_const ((lim seq) / 2);
A3: seq - (seq_const ((lim seq) / 2)) is convergent by A1;
(seq_const ((lim seq) / 2)) . 0 = (lim seq) / 2 by SEQ_1:57;
then lim (seq - (seq_const ((lim seq) / 2))) = (((lim seq) / 2) + ((lim seq) / 2)) - ((lim seq) / 2) by A1, SEQ_4:42
.= (lim seq) / 2 ;
then consider n being Nat such that
A4: for m being Nat st n <= m holds
0 < (seq - (seq_const ((lim seq) / 2))) . m by A2, A3, Th4, XREAL_1:215;
take n ; :: thesis: for m being Nat st n <= m holds
(lim seq) / 2 < seq . m
let m be Nat; :: thesis: ( n <= m implies (lim seq) / 2 < seq . m )
assume n <= m ; :: thesis: (lim seq) / 2 < seq . m
then 0 < (seq - (seq_const ((lim seq) / 2))) . m by A4;
then 0 < (seq . m) - ((seq_const ((lim seq) / 2)) . m) by RFUNCT_2:1;
then 0 < (seq . m) - ((lim seq) / 2) by SEQ_1:57;
then 0 + ((lim seq) / 2) < seq . m by XREAL_1:20;
hence (lim seq) / 2 < seq . m ; :: thesis: verum