let r, u be real number ; :: thesis: ( r > 0 & u > 0 implies ex k being Element of NAT st u / (2 |^ k) <= r )
assume that
A1: r > 0 and
A2: u > 0 ; :: thesis: ex k being Element of NAT st u / (2 |^ k) <= r
set t = 1 / r;
reconsider t = 1 / r as Real ;
A4: t > 0 by A1;
A5: r = 1 / t
.= (u * 1) / (u * t) by A2, XCMPLX_1:92
.= u / (u * t) ;
consider n being Element of NAT such that
A6: u * t < n by SEQ_4:10;
A7: 0 < u * t by A2, A4, XREAL_1:131;
then A8: u / (u * t) > u / n by A2, A6, XREAL_1:78;
defpred S₁[ Element of NAT ] means $1 <= 2 |^ $1;
A9: S₁[ 0 ] ;
A10: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A11: k <= 2 |^ k ; :: thesis: S₁[k + 1]
A12: 2 |^ (k + 1) = (2 |^ k) * (2 |^ 1) by NEWTON:13
.= (2 |^ k) * 2 by NEWTON:10
.= (2 |^ k) + (2 |^ k) ;
2 |^ k >= 1 by Th19;
then A13: (2 |^ k) + (2 |^ k) >= (2 |^ k) + 1 by XREAL_1:9;
(2 |^ k) + 1 >= k + 1 by A11, XREAL_1:9;
hence S₁[k + 1] by A12, A13, XXREAL_0:2; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A9, A10);
then n <= 2 |^ n ;
then A14: u / n >= u / (2 |^ n) by A2, A6, A7, XREAL_1:120;
take n ; :: thesis: u / (2 |^ n) <= r
thus u / (2 |^ n) <= r by A5, A8, A14, XXREAL_0:2; :: thesis: verum