Proof of Existence and Uniqueness of the Integer Part of a Real Number

Every step below in which the same quantity is added to both sides of an inequality, or an inequality is negated, is justified by the elementary order arithmetic in an ordered field; the same lemma, with the totality of the order of an ordered field, is what converts a failure of $x<y$ into $y\le x$.

Uniqueness. Suppose $m,n\in\mathbb{Z}$ both satisfy the displayed condition and $m\ne n$; without loss of generality $m<n$. By claim 3 of the arithmetic and discreteness lemma for the integers, $m+1\le n$. Combining $x<m+1$ with $m+1\le n$ and $n\le x$ gives $x<x$, which is false. Hence $m=n$.

Existence. Fix $x\in\mathbb{R}$. By claim 1 of the Archimedean property applied to $-x$, there is $N\in\mathbb{N}$ with $-x<\iota(N)$, that is $-\iota(N)<x$. Put

$$S=\bigl\{k\in\mathbb{N}\;:\;x<-\iota(N)+\iota(k)\bigr\}.$$

The set $S$ is nonempty: by claim 1 of the Archimedean property applied to $x+\iota(N)$ there is $M\in\mathbb{N}$ with $x+\iota(N)<\iota(M)$, hence $x<-\iota(N)+\iota(M)$ and $M\in S$.

By the well-ordering of the natural numbers, $S$ has a least element $k_{0}$. Set

$$n=-\iota(N)+\iota(k_{0})-1 .$$

Since $\iota(N)$ and $\iota(k_{0})$ lie in $\mathbb{Z}$ by the definition of $\mathbb{Z}$, and $1\in\mathbb{Z}$, claim 2 of the arithmetic lemma gives $n\in\mathbb{Z}$.

The upper inequality. Because $k_{0}\in S$ we have $x<-\iota(N)+\iota(k_{0})=n+1$.

The lower inequality. Every natural number is either $1$ or the successor of a natural number: the set $\{1\}\cup\{j+1:j\in\mathbb{N}\}$ contains $1$ and contains $k+1$ whenever it contains $k$, hence equals $\mathbb{N}$ by the principle of induction.

If $k_{0}=1$ then $\iota(k_{0})=\iota(1)=1$ by claim 1 of the properties of the canonical map, so $n=-\iota(N)$, and $n<x$ was established above; in particular $n\le x$.

Otherwise $k_{0}=j+1$ for some $j\in\mathbb{N}$. Then $j<k_{0}$ by the definition of the order on $\mathbb{N}$, so $j\notin S$ by minimality of $k_{0}$; that is, $-\iota(N)+\iota(j)\le x$. By claim 1 of the properties of the canonical map, $\iota(k_{0})=\iota(j+1)=\iota(j)+1$, whence

$$n=-\iota(N)+\iota(j)+1-1=-\iota(N)+\iota(j)\le x .$$

So $n\le x<n+1$, which proves existence. Writing $\lfloor x\rfloor$ for this unique integer, the inequality $\lfloor x\rfloor\le x$ is immediate, and $x<\lfloor x\rfloor+1$ gives $x-1<\lfloor x\rfloor$ on adding $-1$ to both sides.