let n be Nat; :: thesis: for r being Real st r is irrational holds
(c_d r) . (n + 2) >= 2 * ((c_d r) . n)
let r be Real; :: thesis: ( r is irrational implies (c_d r) . (n + 2) >= 2 * ((c_d r) . n) )
assume A1: r is irrational ; :: thesis: (c_d r) . (n + 2) >= 2 * ((c_d r) . n)
then (scf r) . ((n + 1) + 1) > 0 by Th5;
then A4: (scf r) . (n + 2) >= 0 + 1 by INT_1:7;
A5: 0 < (c_d r) . n by A1, Th8;
(c_d r) . n <= (c_d r) . (n + 1) by A1, Th7;
then ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) >= 1 * ((c_d r) . n) by A4, A5, XREAL_1:66;
then (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n) >= (1 * ((c_d r) . n)) + ((c_d r) . n) by XREAL_1:6;
hence (c_d r) . (n + 2) >= 2 * ((c_d r) . n) by REAL_3:def 6; :: thesis: verum