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