[proofplan]
We prove existence by considering all nonnegative remainders obtained by subtracting a nonnegative multiple of $b$ from $a$, and then choosing the least such remainder by the [well-ordering principle](/theorems/721). Minimality forces that remainder to be smaller than $b$, because otherwise one more copy of $b$ could be subtracted. For uniqueness, two divisions are compared by separating the quotient terms from the remainder terms; the bound $0 \le r,r'<b$ prevents a nonzero multiple of $b$ from occurring as the difference of the remainders.
[/proofplan]
[step:Choose the least nonnegative remainder]
Let $\mathbb{N}_0=\{0\}\cup \mathbb{N}$. Define the set $S=\{s\in \mathbb{N}_0:\text{ there exists }n\in \mathbb{N}_0\text{ such that }s=a-nb\}$. Here the equality $s=a-nb$ is understood in the integers, with $s$ required to lie in $\mathbb{N}_0$. The set $S$ is nonempty, since $a=a-0b$ and $a\in\mathbb{N}\subset \mathbb{N}_0$. By the well-ordering principle for $\mathbb{N}_0$, there is a least element $r\in S$. By the definition of $S$, choose $q\in\mathbb{N}_0$ such that $r=a-qb$. Equivalently, $a=qb+r$.
[guided]
We want to build a quotient and a remainder without already knowing what either should be. The natural construction is to subtract multiples of $b$ from $a$ and keep only those differences which are still nonnegative.
Let $S=\{s\in \mathbb{N}_0:\text{ there exists }n\in \mathbb{N}_0\text{ such that }s=a-nb\}$. This set records every possible nonnegative remainder obtained from $a$ by subtracting a nonnegative multiple of $b$. The set is nonempty because taking $n=0$ gives $a-0b=a$, and $a\in\mathbb{N}\subset\mathbb{N}_0$. Therefore the well-ordering principle for $\mathbb{N}_0$ applies and gives a least element $r\in S$.
Since $r\in S$, the definition of $S$ gives some $q\in\mathbb{N}_0$ with $r=a-qb$. Rearranging in the integers gives $a=qb+r$. Thus we have found a representation of the required form except that we still need to prove the strict bound $r<b$.
[/guided]
[/step]
[step:Force the least remainder to be smaller than the divisor]
We claim that $r<b$. Suppose instead that $r\ge b$. Since $b\in\mathbb{N}$, we have $b>0$, and hence $r-b\in\mathbb{N}_0$. Using $r=a-qb$, the arithmetic laws give $r-b=a-qb-b=a-(q+1)b$. Thus $r-b\in S$. But $b>0$ implies $r-b<r$, contradicting the minimality of $r$ in $S$. Therefore $r<b$. Together with $r\in\mathbb{N}_0$, this gives $0\le r<b$.
[/step]
[step:Compare two possible divisions]
Suppose $q,r,q',r'\in\mathbb{N}_0$ satisfy
\begin{align*}a=qb+r\end{align*}
and
\begin{align*}
a=q'b+r',
\end{align*}
with $0\le r<b$ and $0\le r'<b$. We prove $q=q'$.
Assume first that $q<q'$. Then $d=q'-q$ is a [natural number](/page/Natural%20Number), so $d\ge 1$. Subtracting $qb$ from both representations gives
\begin{align*}
r=db+r'.
\end{align*}
By [citetheorem:9515], multiplication by the positive natural number $b$ preserves order, so $db\ge b$. Since $r'\ge 0$, addition preserves order, again by [citetheorem:9515], and hence
\begin{align*}
r=db+r'\ge b.
\end{align*}
This contradicts $r<b$.
The case $q'<q$ is identical with the primed and unprimed variables interchanged, giving a contradiction to $r'<b$. By trichotomy for the usual order on $\mathbb{N}_0$, exactly one of $q<q'$, $q=q'$, and $q'<q$ holds. Hence neither $q<q'$ nor $q'<q$ holds, so $q=q'$.
[guided]
Now suppose we have two candidate decompositions:
\begin{align*}a=qb+r\end{align*}
and
\begin{align*}
a=q'b+r',
\end{align*}
where $q,r,q',r'\in\mathbb{N}_0$ and both remainders satisfy $0\le r,r'<b$. The goal is to show that the quotients cannot differ.
Assume, toward a contradiction, that $q<q'$. Define
\begin{align*}
d=q'-q.
\end{align*}
Since $q<q'$, the number $d$ is a positive natural number, so $d\ge 1$. Subtracting $qb$ from the equality $qb+r=q'b+r'$ gives
\begin{align*}
r=(q'-q)b+r'=db+r'.
\end{align*}
Because $b\in\mathbb{N}$ is positive and $d\ge 1$, [citetheorem:9515] implies that multiplication by $b$ preserves the order $1\le d$, so
\begin{align*}
b\le db.
\end{align*}
Also $r'\in\mathbb{N}_0$, so $r'\ge 0$. Adding $r'$ to both sides preserves order by [citetheorem:9515], and therefore
\begin{align*}
b\le db+r'=r.
\end{align*}
This contradicts the assumed remainder bound $r<b$.
The opposite case $q'<q$ gives the same contradiction after interchanging $(q,r)$ with $(q',r')$: it would imply $r'\ge b$, contradicting $r'<b$. By trichotomy for the usual order on $\mathbb{N}_0$, exactly one of $q<q'$, $q=q'$, and $q'<q$ holds. Therefore the two quotients cannot be unequal, and we conclude $q=q'$.
[/guided]
[/step]
[step:Recover equality of the remainders]
Since $q=q'$, the two equalities become $a=qb+r$ and $a=qb+r'$. Cancelling the common term $qb$ in the integers gives $r=r'$. Therefore the pair $(q,r)$ is unique. Combining existence and uniqueness proves the theorem.
[/step]
