let r be Real; :: thesis: for seq being Real_Sequence st ( for n being Nat holds seq . n = 1 / (n + r) ) holds
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p
let seq be Real_Sequence; :: thesis: ( ( for n being Nat holds seq . n = 1 / (n + r) ) implies for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p )
assume A0: for n being Nat holds seq . n = 1 / (n + r) ; :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p )
assume A1: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p
consider n being Nat such that
A3: n > (1 / p) - r by Th3;
take n ; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - 0).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - 0).| < p )
assume A2: n <= m ; :: thesis: |.((seq . m) - 0).| < p
B0: seq . m = 1 / (m + r) by A0;
(1 / p) - r < m by A3, A2, XXREAL_0:2;
then A4: ((1 / p) - r) + r < m + r by XREAL_1:8;
then (p ") " > (m + r) " by A1, XREAL_1:88;
then B1: 1 / (m + r) < p ;
B2: - p < - 0 by A1;
0 <= m + r by A1, A4;
then - p < 1 / (m + r) by B2;
hence |.((seq . m) - 0).| < p by B0, B1, SEQ_2:1; :: thesis: verum