[proofplan] Existence and uniqueness of the floor $\lfloor x \rfloor$ are proved separately. For existence, the Archimedean property provides integers above and below $x$, and the well-ordering principle (applied to the natural numbers) selects the smallest integer exceeding $x$; subtracting $1$ gives $\lfloor x \rfloor$. Uniqueness follows from the fact that two integers satisfying $n \le x < n+1$ would differ by a positive integer less than $1$, which is impossible. [/proofplan] [step:Use the Archimedean property to bound $x$ between two integers] By the [Archimedean property](/theorems/1232) (form (5): $\mathbb{Z}$ is cofinal in both directions), there exist integers $m, M \in \mathbb{Z}$ with $m < x < M$. In particular, the set \begin{align*} S := \{k \in \mathbb{Z} : k > x\} \end{align*} is nonempty (since $M \in S$). [guided] The Archimedean property guarantees that $x$ is not an upper bound for all integers, nor a lower bound. This means integers exist both above and below $x$. The set $S$ of integers strictly exceeding $x$ is therefore nonempty. We will extract its minimum in the next step. [/guided] [/step] [step:Apply the well-ordering principle to find the smallest integer exceeding $x$] Define $k_0 := M - m \in \mathbb{N}$ (since $M > x > m$ gives $M > m$, so $M - m \ge 1$). The set $S' := \{k - m : k \in S, \, k \le M\}$ is a nonempty subset of $\{1, 2, \ldots, k_0\}$ (nonempty because $M - m \in S'$), so by the well-ordering of $\mathbb{N}$, $S'$ has a least element $j_0$. Set $n_1 := j_0 + m$. Then $n_1 \in S$ (so $n_1 > x$) and $n_1$ is the smallest element of $S$ that lies in $\{m+1, \ldots, M\}$. We claim $n_1$ is the smallest element of $S$ overall. If $k \in S$ with $k < n_1$, then $k > x > m$, so $k \ge m + 1$. Also $k < n_1 \le M$, so $k \in \{m+1, \ldots, M\} \cap S$, meaning $k - m \in S'$ with $k - m < j_0$, contradicting minimality of $j_0$. Therefore $n_1 = \min S$. Define $n := n_1 - 1$. Since $n_1$ is the smallest integer with $n_1 > x$, and $n = n_1 - 1$, we have $n \le x$ (otherwise $n > x$ would mean $n \in S$ with $n < n_1$, contradicting minimality). Also $n + 1 = n_1 > x$. Therefore $n \le x < n + 1$. [guided] The argument reduces finding the minimum of $S$ to the well-ordering of $\mathbb{N}$ by shifting: we translate $S \cap \{m+1, \ldots, M\}$ to a subset of $\{1, \ldots, M - m\}$, find its minimum, and translate back. Why do we restrict to $\{m+1, \ldots, M\}$? Because $m < x < M$, any integer $k > x$ satisfies $k \ge m + 1$ (since $k > x > m$ and $k, m \in \mathbb{Z}$ gives $k \ge m + 1$). Similarly, we only need to look up to $M$ because $M$ is already in $S$. So $S = S \cap \{m+1, m+2, \ldots\}$, and the minimum of $S$ lies in $\{m+1, \ldots, M\}$. Once $n_1 = \min S$ is found, $n = n_1 - 1$ is the greatest integer $\le x$: it satisfies $n \le x$ (since $n + 1 = n_1 > x$ and $n_1$ is the minimum of $S$, $n = n_1 - 1 \notin S$, so $n \le x$) and $n + 1 > x$. [/guided] [/step] [step:Prove uniqueness of $n$] Suppose $n, n' \in \mathbb{Z}$ both satisfy $n \le x < n + 1$ and $n' \le x < n' + 1$. Then $n \le x < n' + 1$ gives $n < n' + 1$, so $n \le n'$ (since $n, n' \in \mathbb{Z}$). By symmetry, $n' \le n$. Therefore $n = n'$. [guided] If two integers $n$ and $n'$ both satisfy the floor condition, then from $n \le x < n'+1$ we get $n - n' < 1$, and from $n' \le x < n+1$ we get $n' - n < 1$. Since $n - n'$ is an integer with $|n - n'| < 1$, we conclude $n - n' = 0$. [/guided] [/step]