let n be Nat; :: thesis: 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)))
let r be Real; :: thesis: ( r is irrational implies (((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))) )
assume A1: r is irrational ; :: thesis: (((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)))
then A3: (c_d r) . (n + 1) <> 0 by Th8;
A4: (((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n) <> 0 by A1, Th12;
A5: (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - r = (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) / ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))) by A1, Th14
.= ((((c_n r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))) - (((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) * ((c_d r) . (n + 1)))) / (((c_d r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))) by A3, A4, XCMPLX_1:130 ;
(((c_n r) . (n + 1)) * ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))) - (((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) * ((c_d r) . (n + 1))) = ((((((c_n r) . (n + 1)) * ((c_d r) . (n + 1))) * ((rfs r) . (n + 2))) + (((c_n r) . (n + 1)) * ((c_d r) . n))) - ((((c_n r) . (n + 1)) * ((c_d r) . (n + 1))) * ((rfs r) . (n + 2)))) - (((c_n r) . n) * ((c_d r) . (n + 1)))
.= (- 1) |^ n by REAL_3:64 ;
hence (((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))) by A5; :: thesis: verum