today I tried to prove that $<_{\mathbb{Q}}$ is well-defined on $\mathbb{Q} := (\mathbb{Z}\times(\mathbb{Z}-\{0\})) / \asymp$. I'd like to know if the logical structure of the proof is correct since the definition of $<_{\mathbb{Q}}$ uses two implications, and it was somewhat confusing for me at first. If the proof is correct, or if there are any errors, please let me know. Thank you :).
Definition 0. Let $\mathbb{Z}$ be the set of integers with its usual operations and properties.
Definition 1. Let $\asymp$ be the relation on $\mathbb{Z} \times\left ( \mathbb{Z}-\left \{ 0 \right \} \right )$ defined by
$$(x,y)\asymp(z,w) \iff xw=yz, \space\text{for all} \space(x,y),(z,w) \in \mathbb{Z} \times\left ( \mathbb{Z}-\left \{ 0 \right \} \right ).$$
It is easy to verify that $\asymp$ is an equivalence relation.
Definition 2. Define the set of rational numbers $\mathbb{Q}$, as the quotient set of $\mathbb{Z} \times\left ( \mathbb{Z}-\left \{ 0 \right \} \right )$ by $\asymp$. That is,
$$\mathbb{Q} = (\mathbb{Z} \times\left ( \mathbb{Z}-\left \{ 0 \right \} \right )) / \asymp.$$
Definition 3. Let $<_{\mathbb{Q}}$ be the relation defined on $\mathbb{Q}$ by
$$[(x,y)]_{\asymp} <_{\mathbb{Q}} [(z,w)]_{\asymp} \iff \begin{cases} xw<yz & \text{ if } \left ( y>0 \land w>0 \right ) \vee \left ( y<0 \land w<0 \right ) \\ xw>yz & \text{ if } \left ( y>0 \land w<0 \right ) \vee \left ( y<0 \land w>0 \right ) \end{cases}$$
for all $[(x,y)]_{\asymp},[(z,w)]_{\asymp} \in \mathbb{Q}$.
Proposition. The relation $<_{\mathbb{Q}}$ is well-defined on $\mathbb{Q}$, that is, if $[(x,y)]_{\asymp}=[(x',y')]_{\asymp}$ and $[(z,w)]_{\asymp}=[(z',w')]_{\asymp}$, then
$$[(x,y)]_{\asymp} <_{\mathbb{Q}} [(z,w)]_{\asymp} \iff [(x',y')]_{\asymp} <_{\mathbb{Q}} [(z',w')]_{\asymp}.$$
Proof. Let $[(x,y)]_{\asymp}=[(x',y')]_{\asymp}$ and $[(z,w)]_{\asymp}=[(z',w')]_{\asymp}$. Assume that $[(x,y)]_{\asymp} <_{\mathbb{Q}} [(z,w)]_{\asymp}$. Then $xy'=x'y$ and $zw'=z'w$. By Trichotomy and given that $y \neq 0$ and $w \neq 0$, it follows that $y>0$ or $y<0$, and $w>0$ or $w<0$. We proceed by cases.
Case 1. Let $y>0$ and $w>0$, or $y<0$ and $w<0$. Then $xw<yz$ and $yw>0$. Suppose that $y'>0$ and $w'>0$, or $y'<0$ and $w'<0$. Then $y'w'>0$, and hence,
$$xw<yz \implies (xw)(y'w')<(yz)(y'w') \implies (xy')(ww') < (zw')(yy') \implies (x'y)(ww')<(z'w)(yy') \implies (x'w')(yw)<(y'z')(yw).$$
Therefore $x'w'<y'z'$ given that $yw>0$.
Case 2. Let $y>0$ and $w<0$, or $y<0$ and $w>0$. Then $xw>yz$ and $yw<0$. Suppose that $y'>0$ and $w'<0$, or $y'<0$ and $w'>0$. Then $y'w'<0$, and hence by Case 1,
$$xw>yz \implies (xw)(y'w')<(yz)(y'w') \implies (x'w')(yw)<(y'z')(yw).$$
Therefore $x'w'>y'z'$ given that $yw<0$.
Consequently, $[(x,y)]_{\asymp} <_{\mathbb{Q}} [(z,w)]_{\asymp} \implies [(x',y')]_{\asymp} <_{\mathbb{Q}} [(z',w')]_{\asymp}$. Since the reverse implication can be shown to be true in a similar way, we conclude that the relation $<_{\mathbb{Q}}$ is well-defined on $\mathbb{Q}$.