theorem Th5: :: DIOPHAN2:10

for n being Nat
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)) )