theorem Th3: :: DIOPHAN2:8

for r being 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)))