The Relation, Operations, Order and Embedding Defining the Rational Numbers Exist

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}$, $\approx$ and $[x,m]$ be as in Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order §equivalence; and let $\mathbb{Q}$, its sum $+$, product $\cdot$, negation $-$ and order $\le$, and $j$ be as in The Rational Numbers §rationals, The Rational Numbers §operations and The Rational Numbers §embedding.

¶ There is exactly one relation $R$ on $Q$ such that, for all $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$, $((x,m),(y,n))\in R$ if and only if $x\,\iota(n)=y\,\iota(m)$; and $\approx$ is this relation.

¶ $+$ and $\cdot$ are binary operations on $\mathbb{Q}$, $u\mapsto-u$ is a map from $\mathbb{Q}$ to $\mathbb{Q}$, and $\le$ is a relation on $\mathbb{Q}$, 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).$$

¶ $j$ is a map from $\mathbb{Z}$ to $\mathbb{Q}$ with $j(x)=[x,1]$ for every $x\in\mathbb{Z}$, and it is the only such map.