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