let r be Real; :: thesis: for seq being Real_Sequence st seq is convergent & r < lim seq holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
r < seq . k
let seq be Real_Sequence; :: thesis: ( seq is convergent & r < lim seq implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
r < seq . k )
assume A1: ( seq is convergent & r < lim seq ) ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
r < seq . k
reconsider s = NAT --> r as Real_Sequence ;
A3: seq - s is convergent by A1, SEQ_2:25;
s . 0 = r by FUNCOP_1:13;
then lim s = r by SEQ_4:40;
then lim (seq - s) = (lim seq) - r by A1, SEQ_2:26;
then 0 < lim (seq - s) by A1, XREAL_1:52;
then consider n being Element of NAT such that
A4: for k being Element of NAT st n <= k holds
0 < (seq - s) . k by A3, LIMFUNC1:29;
take n ; :: thesis: for k being Element of NAT st n <= k holds
r < seq . k
let k be Element of NAT ; :: thesis: ( n <= k implies r < seq . k )
assume n <= k ; :: thesis: r < seq . k
then 0 < (seq - s) . k by A4;
then 0 < (seq . k) - (s . k) by RFUNCT_2:6;
then 0 < (seq . k) - r by FUNCOP_1:13;
then 0 + r < seq . k by XREAL_1:22;
hence r < seq . k ; :: thesis: verum