Proof of Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order

Write $0$ for $0_{\mathbb{Z}}$. Since $\mathbb{Z}$ is a commutative ring by The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements §ring, sums and products of integers are rearranged by associativity, commutativity and distributivity, and brackets in iterated products are omitted; $\iota(mn)=\iota(m)\iota(n)$ for $m,n\in\mathbb{N}$ by The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements §embedding; and products of natural numbers are natural numbers by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §operations.

Pairs. $Q$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set, as $\mathbb{Z}$ (The Integers §integers) and $\mathbb{N}$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets) are sets. By The Cartesian Product of Two Classes §product and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, the elements of $Q$ are exactly the ordered pairs $(x,m)$ with $x\in\mathbb{Z}$ and $m\in\mathbb{N}$, and the components of $p=(x,m)$ are $p_1=x\in\mathbb{Z}$ and $p_2=m\in\mathbb{N}$. So, for $p,q\in Q$: $\iota(p_2),\iota(q_2)\in\mathbb{Z}$, as $\iota:\mathbb{N}\to\mathbb{Z}$ (The Integers §embedding); sums, products and negatives of integers are integers by The Integers §operations; and $p_2q_2\in\mathbb{N}$.

The relations $\approx$ and $\preceq$. As in the statement, $\approx$ is the relation on the set $Q$ given by Maps and Relations Given by Formulas §relation with the formula $p_1\iota(q_2)=q_1\iota(p_2)$, whose defined set symbols are used properly for $p,q\in Q$ by the paragraph on pairs. Let $\preceq$ be the relation on $Q$ given by the same clause with the formula $p_1\iota(q_2)\le q_1\iota(p_2)$. For $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$, $(x,m)$ and $(y,n)$ lie in $Q$ with components $x,m$ and $y,n$, so

$$(x,m)\approx(y,n)\iff x\iota(n)=y\iota(m),\qquad(1)$$ $$(x,m)\preceq(y,n)\iff x\iota(n)\le y\iota(m).\qquad(2)$$

Positive integers. For $m,n\in\mathbb{N}$, $0<\iota(m)$ by The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements §positive, so $\iota(m)\neq0$ by The Integers §operations; and $0<\iota(m)\iota(n)$ by The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements §positive, since $\iota(m)\iota(n)=\iota(mn)$ with $mn\in\mathbb{N}$.

The clause equivalence above. Let $(x,m),(y,n),(z,k)\in Q$. Reflexive: $x\iota(m)=x\iota(m)$, so $(x,m)\approx(x,m)$ by (1). Symmetric: if $(x,m)\approx(y,n)$, then $x\iota(n)=y\iota(m)$ by (1), so $y\iota(m)=x\iota(n)$ and $(y,n)\approx(x,m)$ by (1). Transitive: if $(x,m)\approx(y,n)$ and $(y,n)\approx(z,k)$, then $x\iota(n)=y\iota(m)$ and $y\iota(k)=z\iota(n)$ by (1), so

$$x\iota(k)\iota(n)=x\iota(n)\iota(k)=y\iota(m)\iota(k)=y\iota(k)\iota(m)=z\iota(n)\iota(m)=z\iota(m)\iota(n).$$

Since $\iota(n)\neq0$, The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements §cancellation gives $x\iota(k)=z\iota(m)$, so $(x,m)\approx(z,k)$ by (1). As $\approx$ is a relation on the set $Q$, it is an equivalence relation on $Q$ by Reflexive, Symmetric, Antisymmetric and Transitive Relations on a Set §reflexive, Reflexive, Symmetric, Antisymmetric and Transitive Relations on a Set §symmetric, Reflexive, Symmetric, Antisymmetric and Transitive Relations on a Set §transitive and Equivalence Relations on a Set §equivalence.

The clause equal above. $Q/{\approx}$ is a set by Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §quotient-set. By The Quotient of a Set by an Equivalence Relation and the Canonical Projection §quotient and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, each class $[p]$ being a set by The Equivalence Class of an Element under an Equivalence Relation §class, the elements of $Q/{\approx}$ are exactly the classes $[p]$ with $p\in Q$, that is, by the paragraph on pairs, exactly the classes $[x,m]$ with $x\in\mathbb{Z}$ and $m\in\mathbb{N}$. For such $x,m$ and $y\in\mathbb{Z}$, $n\in\mathbb{N}$, $(x,m),(y,n)\in Q$, so Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §equal gives $[x,m]=[y,n]$ if and only if $(x,m)\approx(y,n)$, that is, by (1), if and only if $x\iota(n)=y\iota(m)$.

Operations on $Q$. By the paragraph on pairs and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, for $p,q\in Q$ the pairs $(p_1\iota(q_2)+q_1\iota(p_2),p_2q_2)$, $(p_1q_1,p_2q_2)$ and $(-p_1,p_2)$ lie in $Q$. By Maps and Relations Given by Formulas §binary, applied with $c=d=b=Q$, there are binary operations $\oplus$ and $\otimes$ on $Q$ (Binary Operations on a Set §operation) whose values, written as in Binary Operations on a Set §notation, are

$$(x,m)\oplus(y,n)=(x\iota(n)+y\iota(m),mn),\qquad(x,m)\otimes(y,n)=(xy,mn)$$

for $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$; by Maps and Relations Given by Formulas §map there is a map $\ominus:Q\to Q$ with $\ominus((x,m))=(-x,m)$.

Compatibility. Let $p=(x,m)$, $p'=(x',m')$, $q=(y,n)$ and $q'=(y',n')$ be elements of $Q$ with $p\approx p'$ and $q\approx q'$, that is, by (1),

$$x\iota(m')=x'\iota(m),\qquad y\iota(n')=y'\iota(n).\qquad(3)$$

Sum. By (3),

$$(x\iota(n)+y\iota(m))\iota(m'n')=x\iota(m')\iota(n)\iota(n')+y\iota(n')\iota(m)\iota(m')=x'\iota(m)\iota(n)\iota(n')+y'\iota(n)\iota(m)\iota(m')=(x'\iota(n')+y'\iota(m'))\iota(mn),$$

so $p\oplus q\approx p'\oplus q'$ by (1).

Product. By (3), $xy\,\iota(m'n')=x\iota(m')\,y\iota(n')=x'\iota(m)\,y'\iota(n)=x'y'\,\iota(mn)$, so $p\otimes q\approx p'\otimes q'$ by (1).

Negation. By The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements §negation and (3), $(-x)\iota(m')=-(x\iota(m'))=-(x'\iota(m))=(-x')\iota(m)$, so $\ominus(p)\approx\ominus(p')$ by (1).

Order. Let $w=\iota(m')\iota(n')$ and $v=\iota(m)\iota(n)$; then $0<w$ and $0<v$ by the paragraph on positive integers. By (3),

$$x\iota(n)\,w=x\iota(m')\iota(n)\iota(n')=x'\iota(m)\iota(n)\iota(n')=x'\iota(n')\,v,\qquad y\iota(m)\,w=y\iota(n')\iota(m)\iota(m')=y'\iota(n)\iota(m)\iota(m')=y'\iota(m')\,v.$$

Hence, by (2), The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements §positive-factor with $w$, these identities, and The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements §positive-factor with $v$,

$$p\preceq q\iff x\iota(n)\le y\iota(m)\iff x'\iota(n')\,v\le y'\iota(m')\,v\iff x'\iota(n')\le y'\iota(m')\iff p'\preceq q'.$$

The clause operations above. By the compatibility of $\oplus$ and Compatible Operations, Maps and Relations Pass to the Quotient §operation, applied to the set $Q$ and the equivalence relation $\approx$, there is a binary operation $+$ on $Q/{\approx}$ with $[p]+[q]=[p\oplus q]$ for all $p,q\in Q$, that is, $[x,m]+[y,n]=[x\iota(n)+y\iota(m),mn]$. In the same way Compatible Operations, Maps and Relations Pass to the Quotient §operation applied to $\otimes$ gives $\cdot$ with $[x,m]\cdot[y,n]=[xy,mn]$; Compatible Operations, Maps and Relations Pass to the Quotient §map applied to $\ominus$ gives a map $u\mapsto-u$ from $Q/{\approx}$ to itself with $-[x,m]=[-x,m]$; and Compatible Operations, Maps and Relations Pass to the Quotient §relation applied to $\preceq$ gives a relation $\le$ on $Q/{\approx}$ with $[x,m]\le[y,n]$ if and only if $(x,m)\preceq(y,n)$, that is, by (2), if and only if $x\iota(n)\le y\iota(m)$.

For uniqueness, recall that every element of $Q$ is a pair $(x,m)$ with $x\in\mathbb{Z}$ and $m\in\mathbb{N}$. If $+'$ is a binary operation on $Q/{\approx}$ satisfying the stated formula for all $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$, then $[p]+'[q]=[p\oplus q]$ for all $p,q\in Q$, so $+'=+$ by the uniqueness in Compatible Operations, Maps and Relations Pass to the Quotient §operation; in the same way $\cdot$ is unique by Compatible Operations, Maps and Relations Pass to the Quotient §operation and $u\mapsto-u$ by Compatible Operations, Maps and Relations Pass to the Quotient §map. If $\le'$ is a relation on $Q/{\approx}$ with $[x,m]\le'[y,n]$ if and only if $x\iota(n)\le y\iota(m)$, for all $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$, then by (2), for all $p,q\in Q$, $([p],[q])\in{\le'}$ if and only if $(p,q)\in{\preceq}$, so $\le'=\le$ by the uniqueness in Compatible Operations, Maps and Relations Pass to the Quotient §relation.