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

Integers are 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). By The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (vi), sums, products, differences and the order of integers agree whether formed in $\mathbb{Z}$ or in $\mathbb{R}$; as $\mathbb{Z}$ is a commutative ring (The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements (i)) totally ordered by its order (The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements (ii)), sums, products and differences of integers, formed in $\mathbb{R}$, are integers, and $2$, a natural number, is an integer. For $x\in\mathbb{R}$, $\lfloor x\rfloor\in\mathbb{Z}$ and $\lfloor x\rfloor\le x<\lfloor x\rfloor+1$, by The Integer Part of a Real Number (i).

Greatest integer below. Let $n\in\mathbb{Z}$. If $n\le\lfloor z\rfloor$, then $n\le z$, as $\lfloor z\rfloor\le z$. Conversely let $n\le z$, and suppose $n\le\lfloor z\rfloor$ fails. As the order of $\mathbb{Z}$ is total and agrees with that of $\mathbb{R}$, $\lfloor z\rfloor<n$, so $\lfloor z\rfloor+1\le n$ by Discreteness of the Integers (i). Then $z<\lfloor z\rfloor+1\le n\le z$, a contradiction. Hence $n\le\lfloor z\rfloor$.

Doubling. Let $n=\lfloor z\rfloor$, so $2n$, $2n+1$ and $2n+2$ are integers. From $n\le z$ we get $2n\le2z$, so $2n\le\lfloor2z\rfloor$ by (i), applied to the real number $2z$. From $z<n+1$ we get $\lfloor2z\rfloor\le2z<2n+2$. Suppose $\lfloor2z\rfloor\le2n+1$ fails; then $2n+1<\lfloor2z\rfloor$, as the order of $\mathbb{Z}$ is total, and Discreteness of the Integers (i) gives $2n+2\le\lfloor2z\rfloor$, contrary to $\lfloor2z\rfloor<2n+2$. Hence $\lfloor2z\rfloor\le2n+1$.

Powers. Let $m\in\mathbb{N}$. By Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (xii) in the ordered field $\mathbb{R}$ (The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (ii)), with $x=1\ge-1$ and exponent $m$, $2^{m}=(1+1)^{m}\ge1+m\cdot1=1+m>m$, so $m<2^{m}$. The image of $\mathbb{N}$ in $\mathbb{Z}$ is the set of positive integers, by The Integers and the Rational Numbers, with the Natural Numbers and the Integers Identified with Subsets of the Rationals (v), so $0<m$ in $\mathbb{Z}$ and hence in $\mathbb{R}$, by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (vi); thus $0<m<2^{m}$, and in particular $1/m$ is defined. As $2>0$, $2^{m}>0$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (vi), so $2^{-m}=1/2^{m}$ is defined and $0<2^{-m}$. From $0<m<2^{m}$ it follows that $1/2^{m}<1/m$, that is, $2^{-m}<1/m$.