let n be Nat; :: thesis: for r being irrational Real holds
( not n > 1 or |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / ((sqrt 5) * (((c_d r) . n) |^ 2)) or |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)) or |.(r - (((c_n r) . (n + 2)) / ((c_d r) . (n + 2)))).| < 1 / ((sqrt 5) * (((c_d r) . (n + 2)) |^ 2)) )
let r be irrational Real; :: thesis: ( not n > 1 or |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / ((sqrt 5) * (((c_d r) . n) |^ 2)) or |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)) or |.(r - (((c_n r) . (n + 2)) / ((c_d r) . (n + 2)))).| < 1 / ((sqrt 5) * (((c_d r) . (n + 2)) |^ 2)) )
assume that
A2: n > 1 and
A3: ( not |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / ((sqrt 5) * (((c_d r) . n) |^ 2)) & not |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)) & not |.(r - (((c_n r) . (n + 2)) / ((c_d r) . (n + 2)))).| < 1 / ((sqrt 5) * (((c_d r) . (n + 2)) |^ 2)) ) ; :: thesis: contradiction
A4: sqrt 5 > (((c_d r) . (n + 1)) / ((c_d r) . n)) + (1 / (((c_d r) . (n + 1)) / ((c_d r) . n))) by A2, A3, Th3;
set m = n + 1;
n + 1 > 1 + 1 by A2, XREAL_1:8;
then n + 1 > 1 by XXREAL_0:2;
then A7: sqrt 5 > (((c_d r) . ((n + 1) + 1)) / ((c_d r) . (n + 1))) + (1 / (((c_d r) . ((n + 1) + 1)) / ((c_d r) . (n + 1)))) by A3, Th3;
A10: ((c_d r) . (n + 2)) / ((c_d r) . (n + 1)) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) / ((c_d r) . (n + 1)) by REAL_3:def 6
.= (((scf r) . (n + 2)) * (((c_d r) . (n + 1)) * (((c_d r) . (n + 1)) "))) + (((c_d r) . n) / ((c_d r) . (n + 1)))
.= (((scf r) . (n + 2)) * 1) + (((c_d r) . n) / ((c_d r) . (n + 1))) by XCMPLX_0:def 7
.= ((scf r) . (n + 2)) + ((((c_d r) . (n + 1)) / ((c_d r) . n)) ") by XCMPLX_1:213 ;
((c_d r) . (n + 2)) / ((c_d r) . (n + 1)) > ((c_d r) . (n + 1)) / ((c_d r) . (n + 1)) by XREAL_1:74, DIOPHAN1:8;
then A11: ((c_d r) . (n + 2)) / ((c_d r) . (n + 1)) > 1 by XCMPLX_1:60;
set m1 = n - 1;
((c_d r) . ((n - 1) + 2)) / ((c_d r) . ((n - 1) + 1)) > ((c_d r) . ((n - 1) + 1)) / ((c_d r) . ((n - 1) + 1)) by XREAL_1:74, A2, DIOPHAN1:8;
then ((c_d r) . ((n - 1) + 2)) / ((c_d r) . ((n - 1) + 1)) > 1 by XCMPLX_1:60;
then A13: 1 / (((c_d r) . (n + 1)) / ((c_d r) . n)) > ((sqrt 5) - 1) / 2 by A4, Th1;
(scf r) . ((n + 1) + 1) > 0 by DIOPHAN1:5;
then (scf r) . (n + 2) >= 0 + 1 by INT_1:7;
then ((scf r) . (n + 2)) + (1 / (((c_d r) . (n + 1)) / ((c_d r) . n))) > 1 + (((sqrt 5) - 1) / 2) by A13, XREAL_1:8;
hence contradiction by A7, A10, A11, Th1; :: thesis: verum