let r be irrational Real; for n being Nat st n > 1 & |.(r - (((c_n r) . n) / ((c_d r) . n))).| >= 1 / ((sqrt 5) * (((c_d r) . n) |^ 2)) & |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| >= 1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)) holds
sqrt 5 > (((c_d r) . (n + 1)) / ((c_d r) . n)) + (1 / (((c_d r) . (n + 1)) / ((c_d r) . n)))
let n be Nat; ( n > 1 & |.(r - (((c_n r) . n) / ((c_d r) . n))).| >= 1 / ((sqrt 5) * (((c_d r) . n) |^ 2)) & |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| >= 1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)) implies sqrt 5 > (((c_d r) . (n + 1)) / ((c_d r) . n)) + (1 / (((c_d r) . (n + 1)) / ((c_d r) . n))) )
set s5 = sqrt 5;
assume that
A2:
n > 1
and
A3:
|.(r - (((c_n r) . n) / ((c_d r) . n))).| >= 1 / ((sqrt 5) * (((c_d r) . n) |^ 2))
and
A4:
|.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| >= 1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2))
; sqrt 5 > (((c_d r) . (n + 1)) / ((c_d r) . n)) + (1 / (((c_d r) . (n + 1)) / ((c_d r) . n)))
|.(r - (((c_n r) . n) / ((c_d r) . n))).| + |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| = |.((((c_n r) . n) / ((c_d r) . n)) - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).|
by A2, DIOPHAN1:17;
then A6:
|.((((c_n r) . n) / ((c_d r) . n)) - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| >= (1 / ((sqrt 5) * (((c_d r) . n) |^ 2))) + (1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)))
by A3, A4, XREAL_1:7;
A7:
for n being Nat holds (c_d r) . n <> 0
;
A8:
|.((((c_n r) . n) / ((c_d r) . n)) - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| = |.((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))).|
by COMPLEX1:60;
1 / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).| = 1 * ((((c_d r) . (n + 1)) * ((c_d r) . n)) ")
;
then
(((c_d r) . (n + 1)) * ((c_d r) . n)) " >= (1 / ((sqrt 5) * (((c_d r) . n) |^ 2))) + (1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)))
by A6, A7, A8, REAL_3:69;
then A10:
(((c_d r) . (n + 1)) * ((c_d r) . n)) * ((((c_d r) . (n + 1)) * ((c_d r) . n)) ") >= (((c_d r) . (n + 1)) * ((c_d r) . n)) * ((1 / ((sqrt 5) * (((c_d r) . n) |^ 2))) + (1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2))))
by XREAL_1:64;
((c_d r) . n) |^ 2 = ((c_d r) . n) * ((c_d r) . n)
by WSIERP_1:1;
then A15: (((c_d r) . (n + 1)) * ((c_d r) . n)) / ((sqrt 5) * (((c_d r) . n) |^ 2)) =
(((c_d r) . (n + 1)) * ((c_d r) . n)) * (((sqrt 5) ") * ((((c_d r) . n) * ((c_d r) . n)) "))
by XCMPLX_1:204
.=
(((c_d r) . (n + 1)) * ((c_d r) . n)) * (((sqrt 5) ") * ((((c_d r) . n) ") * (((c_d r) . n) ")))
by XCMPLX_1:204
.=
((((sqrt 5) ") * ((c_d r) . (n + 1))) * (((c_d r) . n) * (((c_d r) . n) "))) * (((c_d r) . n) ")
.=
((((sqrt 5) ") * ((c_d r) . (n + 1))) * 1) * (((c_d r) . n) ")
by XCMPLX_0:def 7
.=
(((sqrt 5) ") * ((c_d r) . (n + 1))) * (((c_d r) . n) ")
;
((c_d r) . (n + 1)) |^ 2 = ((c_d r) . (n + 1)) * ((c_d r) . (n + 1))
by WSIERP_1:1;
then ((((c_d r) . (n + 1)) * ((c_d r) . n)) * 1) / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)) =
(((c_d r) . (n + 1)) * ((c_d r) . n)) * (((sqrt 5) ") * ((((c_d r) . (n + 1)) * ((c_d r) . (n + 1))) "))
by XCMPLX_1:204
.=
(((c_d r) . (n + 1)) * ((c_d r) . n)) * (((sqrt 5) ") * ((((c_d r) . (n + 1)) ") * (((c_d r) . (n + 1)) ")))
by XCMPLX_1:204
.=
((((sqrt 5) ") * ((c_d r) . n)) * (((c_d r) . (n + 1)) * (((c_d r) . (n + 1)) "))) * (((c_d r) . (n + 1)) ")
.=
((((sqrt 5) ") * ((c_d r) . n)) * 1) * (((c_d r) . (n + 1)) ")
by XCMPLX_0:def 7
.=
(((sqrt 5) ") * ((c_d r) . n)) * (((c_d r) . (n + 1)) ")
;
then A17:
1 >= ((((sqrt 5) ") * ((c_d r) . (n + 1))) * (((c_d r) . n) ")) + ((((sqrt 5) ") * ((c_d r) . n)) * (((c_d r) . (n + 1)) "))
by A15, A10, XCMPLX_0:def 7;
0 < sqrt 5
by SQUARE_1:20, SQUARE_1:27;
then A18:
(sqrt 5) * 1 >= (sqrt 5) * (((((sqrt 5) ") * ((c_d r) . (n + 1))) * (((c_d r) . n) ")) + ((((sqrt 5) ") * ((c_d r) . n)) * (((c_d r) . (n + 1)) ")))
by A17, XREAL_1:64;
A20: (sqrt 5) * (((((sqrt 5) ") * ((c_d r) . (n + 1))) * (((c_d r) . n) ")) + ((((sqrt 5) ") * ((c_d r) . n)) * (((c_d r) . (n + 1)) "))) =
((((sqrt 5) * ((sqrt 5) ")) * ((c_d r) . (n + 1))) * (((c_d r) . n) ")) + ((((sqrt 5) * ((sqrt 5) ")) * ((c_d r) . n)) * (((c_d r) . (n + 1)) "))
.=
((1 * ((c_d r) . (n + 1))) * (((c_d r) . n) ")) + ((((sqrt 5) * ((sqrt 5) ")) * ((c_d r) . n)) * (((c_d r) . (n + 1)) "))
by SQRT2, XCMPLX_0:def 7
.=
(((c_d r) . (n + 1)) * (((c_d r) . n) ")) + ((1 * ((c_d r) . n)) * (((c_d r) . (n + 1)) "))
by SQRT2, XCMPLX_0:def 7
.=
(((c_d r) . (n + 1)) / ((c_d r) . n)) + (((c_d r) . n) / ((c_d r) . (n + 1)))
;
sqrt 5 <> (((c_d r) . (n + 1)) / ((c_d r) . n)) + (((c_d r) . n) / ((c_d r) . (n + 1)))
by PEPIN:59, IRRAT_1:1;
then
sqrt 5 > (((c_d r) . (n + 1)) / ((c_d r) . n)) + (((c_d r) . n) / ((c_d r) . (n + 1)))
by A18, A20, XXREAL_0:1;
hence
sqrt 5 > (((c_d r) . (n + 1)) / ((c_d r) . n)) + (1 / (((c_d r) . (n + 1)) / ((c_d r) . n)))
by XCMPLX_1:213; verum