let n be Nat; for r being Real st r is irrational holds
(c_d r) . n >= n
let r be Real; ( r is irrational implies (c_d r) . n >= n )
assume A1:
r is irrational
; (c_d r) . n >= n
defpred S1[ Nat] means (c_d r) . $1 >= $1;
A2:
S1[ 0 ]
by REAL_3:def 6;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
set m =
n - 1;
per cases
( n = 0 or n > 0 )
;
suppose
n > 0
;
S1[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
S1[
n + 1]
by A12, XXREAL_0:2;
verum end;
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A3);
hence
(c_d r) . n >= n
; verum