This follows by commutativity of addition in \(\mathbb {N}\).

This follows by commutativity of addition in \(\mathbb {N}\).

Let \(x\), \(y\) and \(z\) in \(\mathrm{MyPreint}\) such that \(x R y\) and \(y R z\). We can write \(x = (a,b)\) and similarly for \(y = (c,d)\) and \(z = (e,f)\). By assumption we have \(a+d=b+c\) and \(c+f=d+e\). Adding these equalities we get

Since addition on \(\mathbb {N}\) is cancellative we get

as wanted.

Clear from Lemma 3, Lemma 4 and Lemma 5.

Let \(x = (a,b)\) and \(x' = (a',b')\), so by assumption \(a + b' = b + a'\). By definition we have

We need to show \(b+a'=b'+a\), which follows immediately from \(a + b' = b + a'\).

Let \(x = (a,b)\), \(y = (c,d)\), \(x' = (a',b')\) and \(y' = (c',d')\) such that \(x \approx x'\) and \(y \approx y'\). by assumption we have

Adding these two equalities we get

and hence

that is \(x + y = (a+c,b+d) \approx (a'+c',b'+d') = x'+y'\).

Let \(x = (a,b)\), \(y = (c,d)\), \(x' = (a',b')\) and \(y' = (c',d')\) such that \(x \approx x'\) and \(y \approx y'\). by assumption we have

Multiplying the first equality by \(c'\) and by \(d'\) we get

and

Multiplying the second equality by \(a\) and by \(b\) we get

and

Adding 1 and 4 we get

Adding 3 and 2 we get

Adding the last two equations and cancelling the terms appearing on both sides we finally have

that is \(x * y \approx x'*y'\).

To prove the lemma it is enough to prove that, for all \(a\), \(b\), \(c\), \(d\), \(e\) and \(f\) in \(\mathbb {N}\), we have

Unravelling the definitions this is

that is true by associativity and commutativity in \(\mathbb {N}\).

We have to prove various properties, namely:

• addition is associative (already done in Lemma 19)

• \(0\) works as neutral element for addition (on both sides)

• existence of an inverse for addition (we prove that \(x + (-x) = (-x) + x = 0\))

• addition is commutative

• left and right distributivity of multiplication with respect to addition

• associativity of multiplication

• \(1\) works as neutral element for multiplication (on both sides)

All the proofs are essentially identical to the proof of Lemma 19 above.

If \(0 = 1\) by definition we would have \(⟦ (0,0) ⟧ = ⟦ (1,0) ⟧\) so \(0+1=0+0\) in \(\mathbb {N}\), that is absurd.

It is enough to prove that, for all \(a\), \(b\), \(c\) and \(d\) in \(\mathbb {N}\) such that \(a \neq b\) and \(c \neq d\) we have \(a*c+b*d\neq a*d+b*c\). If this is not the case we must have \(a = b\) or \(c = d\). (Can you see how to prove this in \(\mathbb {N}\)? You cannot use subtraction!) and we are done.

We have \(0 = y*x-z*x=(y-z)*x\). Since \(x \neq 0\) we have by Lemma 22 that \(y-z=0\) and hence \(y=z\).

Clear from the definition.

Clear from the definition.

We have \(i(a+b) = ⟦ (a+b, 0) ⟧\), \(i(a) = ⟦ (a, 0) ⟧\) and \(i(b) = ⟦ (b, 0) ⟧\), so we need to prove that

that is obvious from the definition.

We have \(i(a*b) = ⟦ (a*b, 0) ⟧\), \(i(a) = ⟦ (a, 0) ⟧\) and \(i(b) = ⟦ (b, 0) ⟧\), so we need to prove that

By definition of multiplication we have

and the lemma follows.

Let \(a\) and \(b\) such that \(i(a)=i(b)\). This means \(⟦ (a,0) ⟧ = ⟦ (b,0) ⟧\) so \(a + 0 = 0 + b\) and hence \(a = b\).

We can just take \(n = 0\).

Let \(x\), \(y\) and \(z\) such that \(x \leq y\) and \(y \leq z\). It follows that there exist \(p\) and \(q\) such that \(y = x + i(p)\) and \(z = y + i(q)\). One can now take \(p+q\) to show that \(x \leq z\).

Let \(x\) and \(y\) such that \(x \leq y\) and \(y \leq x\). It follows that there exist \(p\) and \(q\) such that \(y = x + i(p)\) and \(x = y + i(q)\). In particular

Since \(\mathrm{MyInt}\) is a ring, we obtain \(i(p)+i(q) = 0\). Moreover \(i(p+q)=i(p)+i(q)\) and \(i(0)=0\), so \(i(p+q)=i(0)\) and hence, since \(i\) is injective, \(p+q = 0\). Now, \(p\) and \(q\) are natural numbers, so \(p=q=0\) and so \(x=y\).

Let \(x\) and \(y\) by in \(\mathrm{MyInt}\). We can write \(x = ⟦ (a,b) ⟧\) and \(y = ⟦ (c,d) ⟧\) and we need to prove that \(⟦ (a,b) ⟧ \leq ⟦ (c,d) ⟧\) or \(⟦ (c,d) ⟧ \leq ⟦ (a,b) ⟧\). Let’s consider two cases (we use that the order on \(\mathbb {N}\) is total):

• if \(a + d \leq b + c\) let \(e\) be such that \(b + c = a + d + e\). We prove that \(⟦ (a,b) ⟧ \leq ⟦ (c,d) ⟧\) using \(e\). We have

  \[ ⟦ (a,b) ⟧+i(e) = ⟦ (a,b) ⟧ + ⟦ (e,0) ⟧ = ⟦ (a+e,b+0) ⟧ = ⟦ (a+e,b) ⟧ \]

  We have that \(⟦ (a+e,b) ⟧ = ⟦ (c,d) ⟧\) since

  \[ a+e+d=b+d \]

  by our assumption on \(e\) and so \(⟦ (a,b) ⟧ \leq ⟦ (c,d) ⟧\).

• the case \(b + c \leq a + d\) is completely analogous.

Clear.

We use \(1\) (as natural number). We need to prove that \(0 + i(1) = 1\). Unravelling the definitions this is obvious.

• If \(i(a) \leq i(b)\), let \(n\) be such that \(i(b) = i(a)+i(n)=i(a+n)\). We obtain \(b = a + n\) by injectivity of \(i\) and so \(a \leq b\).

• If \(a \leq b\), let \(k\) be such that \(b = a + k\). We can use \(k\) to show that \(i(a) \leq i(b)\).

Let \(n\) be such that \(y = x + i(n)\). It’s immediate that \(n\) also work to show that \(z + x ≤ z + y\).

By Lemma 22 we already know that \(x*y \neq 0\), so it is enough to prove that \(0 \leq x*y\). Since \(0 {\lt} x\), we have in particular that \(0 \leq x\), and let \(n\) be such that \(x = 0 + i(n)\). Similarly, let \(m\) be such that \(y = 0 + i(m)\). We have \(0 + i(n) = i(n)\) and \(0 + i(m) = i(m)\), so we need to prove that \(0 \leq i(n)*i(m)\). We do so using \(n*m\): we have

as required.