The Integer Part as the Greatest Integer Below, the Integer Part of a Double, and Powers of Two

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\mathbb{R}$, its order $\le$ and its operations be as in The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (ii), with natural numbers and integers read in $\mathbb{R}$ as in The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (v), and for $z\in\mathbb{R}$ let $\lfloor z\rfloor$ be the integer part of $z$. Let $z\in\mathbb{R}$.

(i) For every $n\in\mathbb{Z}$: $n\le z$ if and only if $n\le\lfloor z\rfloor$.

(ii) $2\lfloor z\rfloor\le\lfloor 2z\rfloor\le2\lfloor z\rfloor+1$.

(iii) Let $m\in\mathbb{N}$, let $2^{m}$ be the power of $2$ in $\mathbb{R}$, and write $2^{-m}=1/2^{m}$. Then $0<m<2^{m}$ and $0<2^{-m}<1/m$.