[proofplan]
We first verify that the relation records equality of formal differences by checking reflexivity, symmetry, and transitivity using only the arithmetic laws and cancellation in $\mathbb{N}_0$. We then prove that addition, multiplication, and negation are independent of representatives, so the displayed formulas descend to the quotient set. Finally, we verify the ring axioms by reducing every assertion to associativity, commutativity, distributivity, and identity laws in $\mathbb{N}_0$.
[/proofplan]
[step:Verify that the formal-difference relation is an equivalence relation]
We use the following elementary cancellation property of $\mathbb{N}_0$: if $x,y,z \in \mathbb{N}_0$ and $x+z=y+z$, then $x=y$.
Let $(a,b) \in \mathbb{N}_0 \times \mathbb{N}_0$. Since
\begin{align*}
a+b=b+a,
\end{align*}
we have $(a,b)\sim(a,b)$, so $\sim$ is reflexive.
If $(a,b)\sim(c,d)$, then
\begin{align*}
a+d=b+c.
\end{align*}
By symmetry of equality and commutativity of addition,
\begin{align*}
c+b=d+a.
\end{align*}
Thus $(c,d)\sim(a,b)$, so $\sim$ is symmetric.
Suppose $(a,b)\sim(c,d)$ and $(c,d)\sim(e,f)$. Then
\begin{align*}
a+d=b+c
\end{align*}
and
\begin{align*}
c+f=d+e.
\end{align*}
Adding these equalities gives
\begin{align*}
a+d+c+f=b+c+d+e.
\end{align*}
By commutativity and associativity of addition in $\mathbb{N}_0$,
\begin{align*}
(a+f)+(c+d)=(b+e)+(c+d).
\end{align*}
Cancelling $c+d$ gives
\begin{align*}
a+f=b+e.
\end{align*}
Therefore $(a,b)\sim(e,f)$, so $\sim$ is transitive. Hence $\sim$ is an [equivalence relation](/page/Equivalence%20Relation).
[guided]
The relation is designed so that $(a,b)$ represents the intended expression $a-b$. Thus $(a,b)\sim(c,d)$ means that the equality $a-b=c-d$ has been rewritten without subtraction as
\begin{align*}
a+d=b+c.
\end{align*}
We now verify the three equivalence relation axioms directly.
For reflexivity, take an arbitrary pair $(a,b)\in \mathbb{N}_0\times \mathbb{N}_0$. The defining condition for $(a,b)\sim(a,b)$ is
\begin{align*}
a+b=b+a.
\end{align*}
This is true by commutativity of addition in $\mathbb{N}_0$. Therefore every pair is related to itself.
For symmetry, assume $(a,b)\sim(c,d)$. By definition,
\begin{align*}
a+d=b+c.
\end{align*}
To prove $(c,d)\sim(a,b)$, we must prove
\begin{align*}
c+b=d+a.
\end{align*}
The assumed equality can be read in the reverse direction as $b+c=a+d$, and commutativity of addition gives $c+b=d+a$. Hence $(c,d)\sim(a,b)$.
For transitivity, assume $(a,b)\sim(c,d)$ and $(c,d)\sim(e,f)$. These assumptions mean
\begin{align*}
a+d=b+c
\end{align*}
and
\begin{align*}
c+f=d+e.
\end{align*}
Add the two equalities in $\mathbb{N}_0$:
\begin{align*}
a+d+c+f=b+c+d+e.
\end{align*}
The goal is $(a,b)\sim(e,f)$, namely $a+f=b+e$. To isolate those terms, rearrange both sides using associativity and commutativity:
\begin{align*}
(a+f)+(c+d)=(b+e)+(c+d).
\end{align*}
The cancellation law in $\mathbb{N}_0$ applies because $c+d\in\mathbb{N}_0$, so
\begin{align*}
a+f=b+e.
\end{align*}
This is exactly $(a,b)\sim(e,f)$. Thus the relation is reflexive, symmetric, and transitive.
[/guided]
[/step]
[step:Show that addition descends to equivalence classes]
Suppose $(a,b)\sim(a',b')$ and $(c,d)\sim(c',d')$. Then
\begin{align*}
a+b'=b+a'
\end{align*}
and
\begin{align*}
c+d'=d+c'.
\end{align*}
Adding these equalities gives
\begin{align*}
a+c+b'+d'=b+d+a'+c'.
\end{align*}
By associativity and commutativity of addition,
\begin{align*}
(a+c)+(b'+d')=(b+d)+(a'+c').
\end{align*}
Therefore
\begin{align*}
(a+c,b+d)\sim(a'+c',b'+d').
\end{align*}
Hence the formula
\begin{align*}
[a,b]+[c,d]:=[a+c,b+d]
\end{align*}
is well-defined.
[/step]
[step:Show that multiplication descends to equivalence classes]
First fix $(c,d)\in\mathbb{N}_0\times\mathbb{N}_0$ and suppose $(a,b)\sim(a',b')$. Thus
\begin{align*}
a+b'=b+a'.
\end{align*}
Multiplying this equality by $c$ gives
\begin{align*}
ac+b'c=bc+a'c.
\end{align*}
Multiplying it by $d$ gives
\begin{align*}
ad+b'd=bd+a'd.
\end{align*}
Using these two equalities and rearranging terms,
\begin{align*}
(ac+bd)+(a'd+b'c)=(ad+bc)+(a'c+b'd).
\end{align*}
Hence
\begin{align*}
(ac+bd,ad+bc)\sim(a'c+b'd,a'd+b'c).
\end{align*}
Now fix $(a',b')\in\mathbb{N}_0\times\mathbb{N}_0$ and suppose $(c,d)\sim(c',d')$. Applying the preceding argument with the two pairs interchanged gives
\begin{align*}
(a'c+b'd,a'd+b'c)\sim(a'c'+b'd',a'd'+b'c').
\end{align*}
By transitivity of $\sim$,
\begin{align*}
(ac+bd,ad+bc)\sim(a'c'+b'd',a'd'+b'c').
\end{align*}
Therefore the formula
\begin{align*}
[a,b]\cdot[c,d]:=[ac+bd,ad+bc]
\end{align*}
is well-defined.
[guided]
Multiplication is the only well-definedness check where the algebra is not completely immediate. The formula is chosen because it expands the formal product
\begin{align*}
(a-b)(c-d)=ac+bd-ad-bc.
\end{align*}
Since subtraction is not available in $\mathbb{N}_0$, the positive part $ac+bd$ and the negative part $ad+bc$ are stored as the pair $(ac+bd,ad+bc)$.
We first change only the first representative. Fix $(c,d)\in\mathbb{N}_0\times\mathbb{N}_0$ and assume $(a,b)\sim(a',b')$. The assumption is
\begin{align*}
a+b'=b+a'.
\end{align*}
Multiplying by $c$ in $\mathbb{N}_0$ gives
\begin{align*}
ac+b'c=bc+a'c.
\end{align*}
Multiplying by $d$ gives
\begin{align*}
ad+b'd=bd+a'd.
\end{align*}
The target equivalence is
\begin{align*}
(ac+bd,ad+bc)\sim(a'c+b'd,a'd+b'c),
\end{align*}
which means
\begin{align*}
(ac+bd)+(a'd+b'c)=(ad+bc)+(a'c+b'd).
\end{align*}
This equality follows by placing $ac+b'c=bc+a'c$ and $bd+a'd=ad+b'd$ side by side and then using associativity and commutativity of addition.
Now change only the second representative. Fix $(a',b')\in\mathbb{N}_0\times\mathbb{N}_0$ and assume $(c,d)\sim(c',d')$. The same computation, with the roles of the two pairs interchanged, proves
\begin{align*}
(a'c+b'd,a'd+b'c)\sim(a'c'+b'd',a'd'+b'c').
\end{align*}
The first part showed
\begin{align*}
(ac+bd,ad+bc)\sim(a'c+b'd,a'd+b'c),
\end{align*}
and transitivity of $\sim$ now gives
\begin{align*}
(ac+bd,ad+bc)\sim(a'c'+b'd',a'd'+b'c').
\end{align*}
Thus the product class is independent of both representatives.
[/guided]
[/step]
[step:Show that additive inverse descends to equivalence classes]
Suppose $(a,b)\sim(a',b')$. Then
\begin{align*}
a+b'=b+a'.
\end{align*}
By commutativity of addition,
\begin{align*}
b+a'=a+b'.
\end{align*}
Thus
\begin{align*}
(b,a)\sim(b',a').
\end{align*}
Therefore the formula
\begin{align*}
-[a,b]:=[b,a]
\end{align*}
is well-defined.
[/step]
[step:Verify the additive abelian group structure]
Let $[a,b]$, $[c,d]$, and $[e,f]$ be elements of $\mathbb{Z}_{\mathrm{fd}}$.
Associativity of addition follows from associativity of addition in $\mathbb{N}_0$:
\begin{align*}
([a,b]+[c,d])+[e,f]=[a+c+e,b+d+f]=[a,b]+([c,d]+[e,f]).
\end{align*}
Commutativity follows from commutativity of addition in $\mathbb{N}_0$:
\begin{align*}
[a,b]+[c,d]=[a+c,b+d]=[c+a,d+b]=[c,d]+[a,b].
\end{align*}
The class $[0,0]$ is an additive identity because
\begin{align*}
[a,b]+[0,0]=[a,b].
\end{align*}
The inverse of $[a,b]$ is $[b,a]$, since
\begin{align*}
[a,b]+[b,a]=[a+b,a+b].
\end{align*}
Because
\begin{align*}
(a+b)+0=0+(a+b),
\end{align*}
we have $[a+b,a+b]=[0,0]$. Hence $\mathbb{Z}_{\mathrm{fd}}$ is an [abelian group](/page/Abelian%20Group) under addition.
[/step]
[step:Verify multiplication and distributivity]
Let $[a,b]$, $[c,d]$, and $[e,f]$ be elements of $\mathbb{Z}_{\mathrm{fd}}$.
Commutativity of multiplication follows from commutativity of multiplication and addition in $\mathbb{N}_0$:
\begin{align*}
[a,b]\cdot[c,d]=[ac+bd,ad+bc]=[ca+db,cb+da]=[c,d]\cdot[a,b].
\end{align*}
The element $[1,0]$ is a multiplicative identity because
\begin{align*}
[a,b]\cdot[1,0]=[a,b].
\end{align*}
For associativity, compute both sides. First,
\begin{align*}
([a,b]\cdot[c,d])\cdot[e,f]=[(ac+bd)e+(ad+bc)f,(ac+bd)f+(ad+bc)e].
\end{align*}
Expanding in $\mathbb{N}_0$ gives
\begin{align*}
([a,b]\cdot[c,d])\cdot[e,f]=[ace+bde+adf+bcf,acf+bdf+ade+bce].
\end{align*}
Second,
\begin{align*}
[a,b]\cdot([c,d]\cdot[e,f])=[a(ce+df)+b(cf+de),a(cf+de)+b(ce+df)].
\end{align*}
Expanding in $\mathbb{N}_0$ gives
\begin{align*}
[a,b]\cdot([c,d]\cdot[e,f])=[ace+adf+bcf+bde,acf+ade+bce+bdf].
\end{align*}
The two ordered pairs are equal by associativity and commutativity of addition and multiplication in $\mathbb{N}_0$, so multiplication is associative.
For distributivity, compute
\begin{align*}
[a,b]\cdot([c,d]+[e,f])=[a(c+e)+b(d+f),a(d+f)+b(c+e)].
\end{align*}
Expanding gives
\begin{align*}
[a,b]\cdot([c,d]+[e,f])=[ac+ae+bd+bf,ad+af+bc+be].
\end{align*}
On the other hand,
\begin{align*}
([a,b]\cdot[c,d])+([a,b]\cdot[e,f])=[ac+bd+ae+bf,ad+bc+af+be].
\end{align*}
These ordered pairs are equal by commutativity and associativity of addition in $\mathbb{N}_0$. Hence left distributivity holds. Since multiplication is commutative, right distributivity follows from left distributivity. Therefore multiplication is associative, commutative, has identity $[1,0]$, and distributes over addition.
[/step]
[step:Conclude that the quotient is the formal-difference integer ring]
The previous steps show that $\mathbb{Z}_{\mathrm{fd}}$ is an abelian group under addition, that multiplication on $\mathbb{Z}_{\mathrm{fd}}$ is associative and commutative, that $[1,0]$ is a multiplicative identity, and that multiplication distributes over addition. Thus $\mathbb{Z}_{\mathrm{fd}}$ is a commutative ring with identity.
The notation $[a,b]$ records the formal difference $a-b$: the defining equivalence relation identifies two pairs exactly when their cross-sums agree,
\begin{align*}
a+d=b+c,
\end{align*}
which is the subtraction-free form of the equality $a-b=c-d$. Hence this [quotient ring](/page/Quotient%20Ring) is precisely the formal-difference construction of the integers.
[/step]
