let n be Nat; :: thesis: for r being Real holds
( [/((r * (2 |^ n)) - 1)\] / (2 |^ n) < r & r < [\((r * (2 |^ n)) + 1)/] / (2 |^ n) )
let r be Real; :: thesis: ( [/((r * (2 |^ n)) - 1)\] / (2 |^ n) < r & r < [\((r * (2 |^ n)) + 1)/] / (2 |^ n) )
[/((r * (2 |^ n)) - 1)\] < ((r * (2 |^ n)) - 1) + 1 by INT_1:def 7;
then A1: [/((r * (2 |^ n)) - 1)\] / (2 |^ n) < (r * (2 |^ n)) / (2 |^ n) by XREAL_1:74;
((r * (2 |^ n)) + 1) - 1 < [\((r * (2 |^ n)) + 1)/] by INT_1:def 6;
then (r * (2 |^ n)) / (2 |^ n) < [\((r * (2 |^ n)) + 1)/] / (2 |^ n) by XREAL_1:74;
hence ( [/((r * (2 |^ n)) - 1)\] / (2 |^ n) < r & r < [\((r * (2 |^ n)) + 1)/] / (2 |^ n) ) by A1, XCMPLX_1:89; :: thesis: verum