let r, u be Real; :: thesis: ( r > 0 & u > 0 implies ex k being Nat st u / (2 |^ k) <= r )
defpred S₁[ 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 A2, A3, XREAL_1:76;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume k <= 2 |^ k ; :: thesis: S₁[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 S₁[k + 1] by A8, A7, XXREAL_0:2; :: thesis: verum

end;

take n ; :: thesis: u / (2 |^ n) <= r
A9: r = 1 / t
.= (u * 1) / (u * t) by A2, XCMPLX_1:91
.= u / (u * t) ;
A10: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A6);
then u / n >= u / (2 |^ n) by A2, A3, A4, XREAL_1:118;
hence u / (2 |^ n) <= r by A9, A5, XXREAL_0:2; :: thesis: verum