let r be Real; :: thesis: for seq being Real_Sequence st seq is convergent & lim seq < r holds
ex n being Nat st
for k being Nat st n <= k holds
seq . k < r
let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq < r implies ex n being Nat st
for k being Nat st n <= k holds
seq . k < r )
assume that
A1: seq is convergent and
A2: lim seq < r ; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
seq . k < r
reconsider rr = r as Element of REAL by XREAL_0:def 1;
set s = seq_const r;
A3: (seq_const r) - seq is convergent by A1;
(seq_const r) . 0 = r by SEQ_1:57;
then lim (seq_const r) = r by SEQ_4:25;
then lim ((seq_const r) - seq) = r - (lim seq) by A1, SEQ_2:12;
then consider n being Nat such that
A4: for k being Nat st n <= k holds
0 < ((seq_const r) - seq) . k by A2, A3, LIMFUNC1:4, XREAL_1:50;
take n ; :: thesis: for k being Nat st n <= k holds
seq . k < r
let k be Nat; :: thesis: ( n <= k implies seq . k < r )
assume n <= k ; :: thesis: seq . k < r
then 0 < ((seq_const r) - seq) . k by A4;
then 0 < ((seq_const r) . k) - (seq . k) by RFUNCT_2:1;
then 0 < r - (seq . k) by SEQ_1:57;
then 0 + (seq . k) < r by XREAL_1:20;
hence seq . k < r ; :: thesis: verum