theorem Th15: :: DIOPHAN1:14

for n being Nat
for r being Real st r is irrational holds
(((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - r = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n)))