let n be Nat; for r being Real st r is irrational holds
(c_d r) . (n + 2) > (c_d r) . (n + 1)
let r be Real; ( r is irrational implies (c_d r) . (n + 2) > (c_d r) . (n + 1) )
assume A1:
r is irrational
; (c_d r) . (n + 2) > (c_d r) . (n + 1)
then A2:
(scf r) . ((n + 1) + 1) > 0
by Th5;
A3:
n + 2 >= 0 + 1
by XREAL_1:8;
A4:
(c_d r) . (n + 2) = (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)
by REAL_3:def 6;
(c_d r) . n > 0
by A1, Th8;
then A5:
((c_d r) . (n + 2)) - 0 > ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) - ((c_d r) . n)
by A4, XREAL_1:15;
(c_d r) . (n + 1) >= 1
by A1, Th8;
then
((scf r) . (n + 2)) * ((c_d r) . (n + 1)) >= (c_d r) . (n + 1)
by A2, A3, REAL_3:40, XREAL_1:151;
hence
(c_d r) . (n + 2) > (c_d r) . (n + 1)
by A5, XXREAL_0:2; verum