let n be Nat; for r being Real st r is irrational holds
|.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < 1 / (((c_d r) . (n + 1)) * ((c_d r) . (n + 2)))
let r be Real; ( r is irrational implies |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < 1 / (((c_d r) . (n + 1)) * ((c_d r) . (n + 2))) )
assume A1:
r is irrational
; |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < 1 / (((c_d r) . (n + 1)) * ((c_d r) . (n + 2)))
then A2:
(c_d r) . (n + 1) >= 1
by Th8;
A3:
(c_d r) . ((n + 1) + 1) >= 1
by A1, Th8;
((scf r) . (n + 2)) * ((c_d r) . (n + 1)) < ((rfs r) . (n + 2)) * ((c_d r) . (n + 1))
by A1, Th4, A2, XREAL_1:68;
then
(((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n) < (((rfs r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)
by XREAL_1:8;
then A5:
(c_d r) . (n + 2) < (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)
by REAL_3:def 6;
then A6:
((c_d r) . (n + 1)) * ((c_d r) . (n + 2)) < ((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))
by A2, XREAL_1:68;
|.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| =
|.((- 1) * ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - r)).|
.=
|.((- 1) * (((- 1) |^ n) / (((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))))).|
by A1, Th15
.=
|.(((- 1) * ((- 1) |^ n)) / (((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)))).|
.=
|.(((- 1) |^ (n + 1)) / (((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)))).|
by NEWTON:6
.=
|.((- 1) |^ (n + 1)).| / |.(((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))).|
by COMPLEX1:67
.=
1 / |.(((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))).|
by SERIES_2:1
.=
1 / (((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)))
by A2, A3, A5, COMPLEX1:43
;
hence
|.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < 1 / (((c_d r) . (n + 1)) * ((c_d r) . (n + 2)))
by A6, A2, A3, XREAL_1:88; verum