let r, u be Real; :: thesis: ( r > 0 & u > 0 implies ex k being Nat st u / (2 |^ k) <= r )

defpred S_{1}[ 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_{1}[k] holds

S_{1}[k + 1]

A9: r = 1 / t

.= (u * 1) / (u * t) by A2, XCMPLX_1:91

.= u / (u * t) ;

A10: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[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

defpred S

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

S

proof

take
n
; :: thesis: u / (2 |^ n) <= r
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume k <= 2 |^ k ; :: thesis: S_{1}[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_{1}[k + 1]
by A8, A7, XXREAL_0:2; :: thesis: verum

end;assume k <= 2 |^ k ; :: thesis: S

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

A9: r = 1 / t

.= (u * 1) / (u * t) by A2, XCMPLX_1:91

.= u / (u * t) ;

A10: S

for k being Nat holds S

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