let n be Nat; for r being Real st r is irrational holds
( |.((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))).| < |.((r * ((c_d r) . n)) - ((c_n r) . n)).| & |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < |.(r - (((c_n r) . n) / ((c_d r) . n))).| )
let r be Real; ( r is irrational implies ( |.((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))).| < |.((r * ((c_d r) . n)) - ((c_n r) . n)).| & |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < |.(r - (((c_n r) . n) / ((c_d r) . n))).| ) )
assume A1:
r is irrational
; ( |.((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))).| < |.((r * ((c_d r) . n)) - ((c_n r) . n)).| & |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < |.(r - (((c_n r) . n) / ((c_d r) . n))).| )
then A2: r =
((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) / ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))
by Th14
.=
((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) * (1 / ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)))
;
A3:
(((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n) <> 0
by A1, Th12;
A4: ((r * ((c_d r) . (n + 1))) * ((rfs r) . (n + 2))) + (r * ((c_d r) . n)) =
((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) * ((1 / ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)))
by A2
.=
((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) * 1
by A3, XCMPLX_1:106
.=
(((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)
;
A6: - ((r * ((c_d r) . n)) - ((c_n r) . n)) =
((r * ((c_d r) . (n + 1))) * ((rfs r) . (n + 2))) - (((c_n r) . (n + 1)) * ((rfs r) . (n + 2)))
by A4
.=
((rfs r) . (n + 2)) * ((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1)))
;
A7:
1 < (rfs r) . ((n + 1) + 1)
by A1, Th4;
A8: |.((r * ((c_d r) . n)) - ((c_n r) . n)).| =
|.(- ((r * ((c_d r) . n)) - ((c_n r) . n))).|
by COMPLEX1:52
.=
|.(((rfs r) . (n + 2)) * ((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1)))).|
by A6
.=
|.((rfs r) . (n + 2)).| * |.((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))).|
by COMPLEX1:65
.=
((rfs r) . (n + 2)) * |.((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))).|
by A7, COMPLEX1:43
;
A9:
( (c_d r) . (n + 1) >= 1 & (c_d r) . n >= 1 )
by A1, Th8;
|.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| > 0
by A1, Th19;
then A11:
r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) <> 0
by COMPLEX1:47;
A12: (r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))) * ((c_d r) . (n + 1)) =
(r * ((c_d r) . (n + 1))) - ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) * ((c_d r) . (n + 1)))
.=
(r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))
by A9, XCMPLX_1:87
;
then A13:
|.((r * ((c_d r) . n)) - ((c_n r) . n)).| > |.((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))).|
by A7, A8, A9, A11, COMPLEX1:47, XREAL_1:155;
A14: |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| =
|.(((r * ((c_d r) . (n + 1))) / ((c_d r) . (n + 1))) - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).|
by A9, XCMPLX_1:89
.=
|.(((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))) / ((c_d r) . (n + 1))).|
.=
|.((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))).| / |.((c_d r) . (n + 1)).|
by COMPLEX1:67
.=
|.((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))).| / ((c_d r) . (n + 1))
by A9, COMPLEX1:43
;
A15: |.(r - (((c_n r) . n) / ((c_d r) . n))).| =
|.(((r * ((c_d r) . n)) / ((c_d r) . n)) - (((c_n r) . n) / ((c_d r) . n))).|
by A9, XCMPLX_1:89
.=
|.(((r * ((c_d r) . n)) - ((c_n r) . n)) / ((c_d r) . n)).|
.=
|.((r * ((c_d r) . n)) - ((c_n r) . n)).| / |.((c_d r) . n).|
by COMPLEX1:67
.=
|.((r * ((c_d r) . n)) - ((c_n r) . n)).| / ((c_d r) . n)
by A9, COMPLEX1:43
;
A16:
|.((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))).| / ((c_d r) . (n + 1)) < |.((r * ((c_d r) . n)) - ((c_n r) . n)).| / ((c_d r) . (n + 1))
by A9, A13, XREAL_1:74;
|.((r * ((c_d r) . n)) - ((c_n r) . n)).| >= 0
by COMPLEX1:46;
then
|.((r * ((c_d r) . n)) - ((c_n r) . n)).| / ((c_d r) . (n + 1)) <= |.((r * ((c_d r) . n)) - ((c_n r) . n)).| / ((c_d r) . n)
by A1, Th7, A9, XREAL_1:118;
hence
( |.((r * ((c_d r) . (n + 1))) - ((c_n r) . (n + 1))).| < |.((r * ((c_d r) . n)) - ((c_n r) . n)).| & |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < |.(r - (((c_n r) . n) / ((c_d r) . n))).| )
by A7, A8, A9, A11, A12, A14, A15, A16, COMPLEX1:47, XREAL_1:155, XXREAL_0:2; verum