let g, x0 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 that
A1: seq is convergent and
A2: lim seq = x0 and
A3: 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 )
x0 - g < lim seq by A2, A3, Lm1;
then consider k1 being Nat such that
A4: for n being Nat st k1 <= n holds
x0 - g < seq . n by A1, LIMFUNC2:1;
lim seq < x0 + g by A2, A3, Lm1;
then consider k2 being Nat such that
A5: for n being Nat st k2 <= n holds
seq . n < x0 + g by A1, LIMFUNC2:2;
reconsider k = max (k1,k2) as Element of NAT by ORDINAL1:def 12;
take k ; :: 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 A6: k <= n ; :: thesis: ( x0 - g < seq . n & seq . n < x0 + g )
k1 <= k by XXREAL_0:25;
then k1 <= n by A6, XXREAL_0:2;
hence x0 - g < seq . n by A4; :: thesis: seq . n < x0 + g
k2 <= k by XXREAL_0:25;
then k2 <= n by A6, XXREAL_0:2;
hence seq . n < x0 + g by A5; :: thesis: verum