let n be Nat; :: thesis: for r being Real st r is irrational holds
|.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2)
let r be Real; :: thesis: ( r is irrational implies |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2) )
assume A1: r is irrational ; :: thesis: |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2)
|.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2)
proof
per cases ( n = 0 or n > 0 ) ;
suppose A3: n = 0 ; :: thesis: |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2)
then A6: |.(r - (((c_n r) . n) / ((c_d r) . n))).| = |.(r - (((c_n r) . 0) / 1)).| by REAL_3:def 6
.= |.(r - ((scf r) . 0)).| by REAL_3:def 5
.= |.(r - [\((rfs r) . 0)/]).| by REAL_3:def 4
.= |.(r - [\r/]).| by REAL_3:def 3
.= |.(frac r).| by INT_1:def 8
.= frac r by ABSVALUE:def 1, INT_1:43 ;
1 / (((c_d r) . n) |^ 2) = 1 / (((c_d r) . 0) |^ 2) by A3
.= 1 / (1 |^ 2) by REAL_3:def 6
.= 1 ;
hence |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2) by A6, INT_1:43; :: thesis: verum
end;
suppose A8: n > 0 ; :: thesis: |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2)
set m = n - 1;
reconsider m = n - 1 as Nat by A8;
A10: (c_d r) . (m + 1) >= 1 by A1, Th8;
then ((c_d r) . (m + 1)) * ((c_d r) . (m + 1)) >= 1 by XREAL_1:159;
then A12: ((c_d r) . (m + 1)) |^ 2 >= 1 by WSIERP_1:1;
((c_d r) . ((m + 1) + 1)) * ((c_d r) . (m + 1)) >= ((c_d r) . (m + 1)) * ((c_d r) . (m + 1)) by A1, A10, Th7, XREAL_1:64;
then ((c_d r) . (m + 1)) * ((c_d r) . (m + 2)) >= ((c_d r) . (m + 1)) |^ 2 by WSIERP_1:1;
then 1 / (((c_d r) . (m + 1)) * ((c_d r) . (m + 2))) <= 1 / (((c_d r) . (m + 1)) |^ 2) by A12, XREAL_1:85;
hence |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2) by A1, XXREAL_0:2, Th21; :: thesis: verum
end;
end;
end;
hence |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / (((c_d r) . n) |^ 2) ; :: thesis: verum