theorem Th22: :: DIOPHAN1:21

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