let r1, r2 be Real; :: thesis: ( r1 < r2 implies ex n being Nat st [\((r1 * (2 |^ n)) + 1)/] / (2 |^ n) < r2 )
assume r1 < r2 ; :: thesis: ex n being Nat st [\((r1 * (2 |^ n)) + 1)/] / (2 |^ n) < r2
then 0 < r2 - r1 by XREAL_1:50;
then consider k being Nat such that
A1: 1 / (2 |^ k) <= r2 - r1 by PREPOWER:92;
take k + 1 ; :: thesis: [\((r1 * (2 |^ (k + 1))) + 1)/] / (2 |^ (k + 1)) < r2
set K2 = 2 |^ (k + 1);
2 |^ (k + 1) = 2 * (2 |^ k) by NEWTON:6;
then A2: (2 |^ (k + 1)) * (1 / (2 |^ k)) = 2 * ((2 |^ k) * (1 / (2 |^ k)))
.= 2 * 1 by XCMPLX_1:106 ;
(2 |^ (k + 1)) * (r1 + (1 / (2 |^ k))) <= r2 * (2 |^ (k + 1)) by A1, XREAL_1:19, XREAL_1:64;
then ( [\(((2 |^ (k + 1)) * r1) + 1)/] <= (((2 |^ (k + 1)) * r1) + 2) - 1 & (((2 |^ (k + 1)) * r1) + 2) - 1 < (r2 * (2 |^ (k + 1))) - 0 ) by A2, XREAL_1:15, INT_1:def 6;
then [\(((2 |^ (k + 1)) * r1) + 1)/] < (2 |^ (k + 1)) * r2 by XXREAL_0:2;
then ( [\(((2 |^ (k + 1)) * r1) + 1)/] / (2 |^ (k + 1)) < (r2 * (2 |^ (k + 1))) / (2 |^ (k + 1)) & (r2 * (2 |^ (k + 1))) / (2 |^ (k + 1)) = r2 ) by XREAL_1:74, XCMPLX_1:89;
hence [\((r1 * (2 |^ (k + 1))) + 1)/] / (2 |^ (k + 1)) < r2 ; :: thesis: verum