let r1, r2 be Real; :: thesis: ( r1 < r2 implies ex n being Nat st r1 < [/((r2 * (2 |^ n)) - 1)\] / (2 |^ n) )
assume r1 < r2 ; :: thesis: ex n being Nat st r1 < [/((r2 * (2 |^ n)) - 1)\] / (2 |^ n)
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 < [/((r2 * (2 |^ (k + 1))) - 1)\] / (2 |^ (k + 1))
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) + 2) - 2 < (r2 * (2 |^ (k + 1))) - 1 & (r2 * (2 |^ (k + 1))) - 1 <= [/(((2 |^ (k + 1)) * r2) - 1)\] ) by A2, XREAL_1:15, INT_1:def 7;
then (2 |^ (k + 1)) * r1 < [/(((2 |^ (k + 1)) * r2) - 1)\] by XXREAL_0:2;
then ( r1 = (r1 * (2 |^ (k + 1))) / (2 |^ (k + 1)) & (r1 * (2 |^ (k + 1))) / (2 |^ (k + 1)) < [/(((2 |^ (k + 1)) * r2) - 1)\] / (2 |^ (k + 1)) ) by XREAL_1:74, XCMPLX_1:89;
hence r1 < [/((r2 * (2 |^ (k + 1))) - 1)\] / (2 |^ (k + 1)) ; :: thesis: verum