let m, n be Nat; :: thesis: for r being Real st r is irrational & m > n holds
|.(r - (((c_n r) . n) / ((c_d r) . n))).| > |.(r - (((c_n r) . m) / ((c_d r) . m))).|
let r be Real; :: thesis: ( r is irrational & m > n implies |.(r - (((c_n r) . n) / ((c_d r) . n))).| > |.(r - (((c_n r) . m) / ((c_d r) . m))).| )
assume that
A1: r is irrational and
A3: m > n ; :: thesis: |.(r - (((c_n r) . n) / ((c_d r) . n))).| > |.(r - (((c_n r) . m) / ((c_d r) . m))).|
defpred S₁[ Nat] means |.(r - (((c_n r) . n) / ((c_d r) . n))).| > |.(r - (((c_n r) . ((n + 1) + $1)) / ((c_d r) . ((n + 1) + $1)))).|;
A4: S₁[ 0 ] by A1, Th22;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then |.(r - (((c_n r) . n) / ((c_d r) . n))).| > |.(r - (((c_n r) . (((n + 1) + k) + 1)) / ((c_d r) . (((n + 1) + k) + 1)))).| by A1, Th22, XXREAL_0:2;
hence S₁[k + 1] ; :: thesis: verum

end;

A8: for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
m - n > n - n by A3, XREAL_1:14;
then m - n >= 0 + 1 by INT_1:7;
then A9: (m - n) - 1 >= 1 - 1 by XREAL_1:9;
reconsider i = (m - n) - 1 as Integer ;
i in NAT by A9, INT_1:3;
then reconsider i = i as Nat ;
|.(r - (((c_n r) . n) / ((c_d r) . n))).| > |.(r - (((c_n r) . ((n + 1) + i)) / ((c_d r) . ((n + 1) + i)))).| by A8;
hence |.(r - (((c_n r) . n) / ((c_d r) . n))).| > |.(r - (((c_n r) . m) / ((c_d r) . m))).| ; :: thesis: verum