let n be Nat; :: thesis: for r being Real st r is irrational holds
(c_d r) . n >= n
let r be Real; :: thesis: ( r is irrational implies (c_d r) . n >= n )
assume A1: r is irrational ; :: thesis: (c_d r) . n >= n
defpred S₁[ Nat] means (c_d r) . $1 >= $1;
A2: S₁[ 0 ] by REAL_3:def 6;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set m = n - 1;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: S₁[n + 1]

hence S₁[n + 1] by A1, Th8; :: thesis: verum

end;

suppose n > 0 ; :: thesis: S₁[n + 1]

then reconsider m = n - 1 as Nat ;
A7: (scf r) . ((m + 1) + 1) > 0 by A1, Th5;
A8: m + 2 >= 0 + 1 by XREAL_1:8;
(c_d r) . (m + 1) >= 1 by A1, Th8;
then A9: ((scf r) . (m + 2)) * ((c_d r) . (m + 1)) >= (c_d r) . (m + 1) by A7, A8, REAL_3:40, XREAL_1:151;
(((scf r) . (m + 2)) * ((c_d r) . (m + 1))) + ((c_d r) . m) >= ((c_d r) . (m + 1)) + ((c_d r) . m) by A9, XREAL_1:6;
then A12: (c_d r) . (m + 2) >= ((c_d r) . (m + 1)) + ((c_d r) . m) by REAL_3:def 6;
A13: ((c_d r) . (m + 1)) + ((c_d r) . m) >= n + ((c_d r) . m) by A4, XREAL_1:6;
n + ((c_d r) . m) >= n + 1 by A1, Th8, XREAL_1:6;
then ((c_d r) . (m + 1)) + ((c_d r) . m) >= n + 1 by A13, XXREAL_0:2;
hence S₁[n + 1] by A12, XXREAL_0:2; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence (c_d r) . n >= n ; :: thesis: verum