let n be Nat; :: thesis: for r being Real st r is irrational & n is odd holds
r < ((c_n r) . n) / ((c_d r) . n)
let r be Real; :: thesis: ( r is irrational & n is odd implies r < ((c_n r) . n) / ((c_d r) . n) )
assume A1: r is irrational ; :: thesis: ( not n is odd or r < ((c_n r) . n) / ((c_d r) . n) )
assume n is odd ; :: thesis: r < ((c_n r) . n) / ((c_d r) . n)
then reconsider m = n - 1 as natural even number ;
((c_d r) . (m + 1)) * ((((c_d r) . (m + 1)) * ((rfs r) . (m + 2))) + ((c_d r) . m)) > 0 by A1, Th13;
then ((- 1) |^ m) / (((c_d r) . (m + 1)) * ((((c_d r) . (m + 1)) * ((rfs r) . (m + 2))) + ((c_d r) . m))) > 0 ;
then (((c_n r) . (m + 1)) / ((c_d r) . (m + 1))) - r > 0 by A1, Th15;
then ((((c_n r) . (m + 1)) / ((c_d r) . (m + 1))) - r) + r > 0 + r by XREAL_1:8;
hence r < ((c_n r) . n) / ((c_d r) . n) ; :: thesis: verum