let r, u be Real; :: thesis: ( r > 0 & u > 0 implies ex k being Nat st u / (2 |^ k) <= r )
defpred S1[ Nat] means \$1 <= 2 |^ \$1;
assume that
A1: r > 0 and
A2: u > 0 ; :: thesis: ex k being Nat st u / (2 |^ k) <= r
set t = 1 / r;
reconsider t = 1 / r as Real ;
consider n being Nat such that
A3: u * t < n by SEQ_4:3;
A4: 0 < u * t by A1, A2;
then A5: u / (u * t) > u / n by ;
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume k <= 2 |^ k ; :: thesis: S1[k + 1]
then A7: (2 |^ k) + 1 >= k + 1 by XREAL_1:7;
2 |^ k >= 1 by Th11;
then A8: (2 |^ k) + (2 |^ k) >= (2 |^ k) + 1 by XREAL_1:7;
2 |^ (k + 1) = (2 |^ k) * (2 |^ 1) by NEWTON:8
.= (2 |^ k) * 2
.= (2 |^ k) + (2 |^ k) ;
hence S1[k + 1] by ; :: thesis: verum
end;
take n ; :: thesis: u / (2 |^ n) <= r
A9: r = 1 / t
.= (u * 1) / (u * t) by
.= u / (u * t) ;
A10: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A10, A6);
then u / n >= u / (2 |^ n) by ;
hence u / (2 |^ n) <= r by ; :: thesis: verum