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

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let $\mathbb{Z}$, its operations and order, and $\iota$ be as in The Integers §integers, The Integers §operations and The Integers §embedding. Let $Q=\mathbb{Z}\times\mathbb{N}$ and let $\approx$ be the relation on $Q$ with $(x,m)\approx(y,n)$ if and only if $x\,\iota(n)=y\,\iota(m)$, for all $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$, given by Maps and Relations Given by Formulas §relation.

¶ $\approx$ is an equivalence relation on $Q$. Write $Q/{\approx}$ for the quotient and $[x,m]$ for the class of $(x,m)$.

¶ $Q/{\approx}$ is a set whose elements are exactly the classes $[x,m]$ with $x\in\mathbb{Z}$ and $m\in\mathbb{N}$, and for all $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$, $[x,m]=[y,n]$ if and only if $x\,\iota(n)=y\,\iota(m)$.

¶ There are unique binary operations $+$ and $\cdot$ on $Q/{\approx}$, a unique map $u\mapsto-u$ from $Q/{\approx}$ to itself and a unique relation $\le$ on $Q/{\approx}$ such that, for all $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$,

$$[x,m]+[y,n]=[x\,\iota(n)+y\,\iota(m),mn],\quad[x,m]\cdot[y,n]=[xy,mn],\quad-[x,m]=[-x,m],\quad[x,m]\le[y,n]\iff x\,\iota(n)\le y\,\iota(m).$$