Proof of Division with Remainder

Routine facts about nonempty classes and the class of remainders are used without comment (Toolkit for AL1).

Consider the set

$$S=\{r\in\mathbb{N}_{0}: m=qn+r\text{ for some }q\in\mathbb{Z}\}.$$

It is nonempty. If $0\le m$, then $m\in S$, with $q=0$. If $m<0$, take $q=m$: then $m=mn+m(1-n)$, and $m(1-n)\ge0$ because $m<0$ and $1-n\le0$, so $m(1-n)\in S$. (Arithmetic and order of $\mathbb{Z}$ are routine under Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity.)

The order of $\mathbb{N}_{0}$ is a well-order by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (i), so the nonempty set $S$ has a least element $r$ (Well-Orders on a Set (i)). Fix $q\in\mathbb{Z}$ with $m=qn+r$.

We claim $r<n$, which proves existence. Suppose instead that $n\le r$. Then $r-n\in\mathbb{N}_{0}$ and

$$m=(q+1)n+(r-n),$$

so $r-n\in S$; but $r-n<r$ because $1\le n$, contradicting the minimality of $r$.

For uniqueness, let $m=qn+r=q'n+r'$ with $q,q'\in\mathbb{Z}$, $r,r'\in\mathbb{N}_{0}$ and $r,r'<n$. Suppose $q<q'$. Then $q'-q\ge1$ by Discreteness of the Integers (i), so

$$r-r'=(q'-q)n\ge n,$$

whereas $r-r'\le r<n$, a contradiction. Exchanging the roles of the two pairs rules out $q'<q$ in the same way, so $q=q'$, and then $r=m-qn=r'$.