let r be real number ; :: thesis: ( 0 < r implies InvShift r is convergent )
assume A1: 0 < r ; :: thesis: InvShift r is convergent
set seq = InvShift r;
take g = 0c ; :: according to COMSEQ_2:def 4 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= |.(((InvShift r) . b₃) - g).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= |.(((InvShift r) . b₂) - g).| ) )
assume a3: 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= |.(((InvShift r) . b₂) - g).| )
consider k1 being Element of NAT such that
A4: p " < k1 by SEQ_4:10;
take n = k1; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= |.(((InvShift r) . b₁) - g).| )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= |.(((InvShift r) . m) - g).| )
assume A5: n <= m ; :: thesis: not p <= |.(((InvShift r) . m) - g).|
(p " ) + 0 < k1 + r by A1, A4, XREAL_1:10;
then A6: 1 / (k1 + r) < 1 / (p " ) by a3, XREAL_1:78;
n + r <= m + r by A5, XREAL_1:8;
then 1 / (m + r) <= 1 / (n + r) by A1, XREAL_1:120;
then A7: 1 / (m + r) < p by XXREAL_0:2, A6;
(InvShift r) . m = 1 / (m + r) by Def2;
hence abs (((InvShift r) . m) - g) < p by A7, ABSVALUE:def 1, A1; :: thesis: verum