let x0, g be Real; :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & 0 < g holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
( x0 - g < seq . n & seq . n < x0 + g )
let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & 0 < g implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
( x0 - g < seq . n & seq . n < x0 + g ) )
assume A1: ( seq is convergent & lim seq = x0 & 0 < g ) ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
( x0 - g < seq . n & seq . n < x0 + g )
then x0 - g < lim seq by Lm1;
then consider k1 being Element of NAT such that
A2: for n being Element of NAT st k1 <= n holds
x0 - g < seq . n by A1, LIMFUNC2:1;
lim seq < x0 + g by A1, Lm1;
then consider k2 being Element of NAT such that
A3: for n being Element of NAT st k2 <= n holds
seq . n < x0 + g by A1, LIMFUNC2:2;
take k = max k1,k2; :: thesis: for n being Element of NAT st k <= n holds
( x0 - g < seq . n & seq . n < x0 + g )
let n be Element of NAT ; :: thesis: ( k <= n implies ( x0 - g < seq . n & seq . n < x0 + g ) )
assume A4: k <= n ; :: thesis: ( x0 - g < seq . n & seq . n < x0 + g )
k1 <= k by XXREAL_0:25;
then k1 <= n by A4, XXREAL_0:2;
hence x0 - g < seq . n by A2; :: thesis: seq . n < x0 + g
k2 <= k by XXREAL_0:25;
then k2 <= n by A4, XXREAL_0:2;
hence seq . n < x0 + g by A3; :: thesis: verum