let r be Real; :: thesis: ( r is irrational implies for n being Nat holds (c_d r) . (n + 1) >= (c_d r) . n )
assume A1: r is irrational ; :: thesis: for n being Nat holds (c_d r) . (n + 1) >= (c_d r) . n
defpred S1[ Nat] means (c_d r) . $1 <= (c_d r) . ($1 + 1);
A2: S1[ 0 ]
proof
A3: (c_d r) . 0 = 1 by REAL_3:def 6;
(rfs r) . (0 + 1) > 1 by A1, Th4;
then ((rfs r) . 1) - 1 > 1 - 1 by XREAL_1:14;
then [\((rfs r) . 1)/] > 0 by INT_1:def 6;
then (scf r) . 1 > 0 by REAL_3:def 4;
then 0 + 1 <= (scf r) . 1 by INT_1:7;
hence S1[ 0 ] by A3, REAL_3:def 6; :: thesis: verum
end;
A8: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; :: thesis: S1[n + 1]
A9: ((c_d r) . (n + 2)) - ((c_d r) . (n + 1)) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) - ((c_d r) . (n + 1)) by REAL_3:def 6
.= ((((scf r) . (n + 2)) - 1) * ((c_d r) . (n + 1))) + ((c_d r) . n) ;
A10: (scf r) . (n + 2) = [\((rfs r) . (n + 2))/] by REAL_3:def 4;
(rfs r) . ((n + 1) + 1) > 1 by A1, Th4;
then ((rfs r) . (n + 2)) - 1 > 1 - 1 by XREAL_1:14;
then (scf r) . (n + 2) > 0 by A10, INT_1:def 6;
then 0 + 1 <= (scf r) . (n + 2) by INT_1:7;
then A12: ((scf r) . (n + 2)) - 1 >= 1 - 1 by XREAL_1:13;
( (c_d r) . (n + 1) >= 0 & (c_d r) . n >= 0 ) by REAL_3:51;
then (((c_d r) . (n + 2)) - ((c_d r) . (n + 1))) + ((c_d r) . (n + 1)) >= 0 + ((c_d r) . (n + 1)) by A9, A12, XREAL_1:6;
hence S1[n + 1] ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A2, A8);
 hence for n being Nat holds (c_d r) . (n + 1) >= (c_d r) . n ; :: thesis: verum