let r be Real; :: thesis: for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / (n + r) ) holds
seq is convergent
let seq be Real_Sequence; :: thesis: ( 0 <= r & ( for n being Nat holds seq . n = 1 / (n + r) ) implies seq is convergent )
assume that
A1: 0 <= r and
A2: for n being Nat holds seq . n = 1 / (n + r) ; :: thesis: seq is convergent
take 0 ; :: according to SEQ_2:def 6 :: thesis: for b₁ being set holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.((seq . b₃) - 0).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.((seq . b₂) - 0).| ) )
assume A3: 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.((seq . b₂) - 0).| )
consider k1 being Nat such that
A4: p " < k1 by Th3;
(p ") + 0 < k1 + r by A1, A4, XREAL_1:8;
then 1 / (k1 + r) < 1 / (p ") by A3, XREAL_1:76;
then A5: 1 / (k1 + r) < 1 * ((p ") ") by XCMPLX_0:def 9;
take n = k1; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= |.((seq . b₁) - 0).| )
let m be Nat; :: thesis: ( not n <= m or not p <= |.((seq . m) - 0).| )
assume n <= m ; :: thesis: not p <= |.((seq . m) - 0).|
then A6: n + r <= m + r by XREAL_1:6;
0 < p " by A3;
then 1 / (m + r) <= 1 / (n + r) by A1, A4, A6, XREAL_1:118;
then A7: 1 / (m + r) < p by A5, XXREAL_0:2;
seq . m = 1 / (m + r) by A2;
hence not p <= |.((seq . m) - 0).| by A1, A7, ABSVALUE:def 1; :: thesis: verum