let x be real number ; :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x holds
for eps being real number st eps > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
seq . n > x - eps
let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x implies for eps being real number st eps > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
seq . n > x - eps )
assume A1: ( seq is convergent & lim seq = x ) ; :: thesis: for eps being real number st eps > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
seq . n > x - eps
let eps be real number ; :: thesis: ( eps > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
seq . n > x - eps )
assume eps > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
seq . n > x - eps
then consider N being Element of NAT such that
A2: for n being Element of NAT st n >= N holds
abs ((seq . n) - x) < eps by A1, SEQ_2:def 7;
take N ; :: thesis: for n being Element of NAT st n >= N holds
seq . n > x - eps
let n be Element of NAT ; :: thesis: ( n >= N implies seq . n > x - eps )
assume n >= N ; :: thesis: seq . n > x - eps
then abs ((seq . n) - x) < eps by A2;
then (seq . n) - x > - eps by SEQ_2:1;
then ((seq . n) - x) + x > (- eps) + x by XREAL_1:6;
hence seq . n > x - eps ; :: thesis: verum