I'm using the following definitiosn for addition $+$, multiplication $\cdot$, and the relation $\preceq$ on the set of integers: \begin{align*}\tag{I} [(a,b)]+[(c,d)]&:=[(a+c,b+d)] \\ \tag{II} [(a,b)]\cdot [(c,d)]&:=[(ac+bd,ad+bc)]. \\ \tag{III} [(a,b)]\preceq [(c,d)]&:\Leftrightarrow a+d\leq b+c \end{align*}
I already proved that for all natural numbers $a,b,c\in\mathbb{N}$ we have that \begin{align*}\tag{IV} a\leq b\Leftrightarrow ac\leq bc. \end{align*}
Now I want to show that for all $x,y,z\in\mathbb{Z}$ with $z>0$ we have that \begin{align*} x\preceq y\Leftrightarrow xz\preceq yz. \end{align*}
I tried the following approach: Let $x=[(a,b)], y=[(c,d)]$, and $z=[(e,f)]$. From Definition (III) we have \begin{align*} [(a,b)]\preceq [(c,d)]\Leftrightarrow a+d\leq b+c. \end{align*} From (IV) we know that there exists some $u\in\mathbb{N}$ such that \begin{align*}\tag{V} a+d\leq b+c\Leftrightarrow (a+d)\cdot u\leq (b+c)\cdot u. \end{align*}
At this point I got stuck, so I tried to start with the other side of the equivalence I'm trying to prove, i.e. \begin{align*}\tag{VI} [(a,b)]\cdot[(e,f)]\preceq [(c,d)]\cdot[(e,f)]. \end{align*}
From (II) we have that \begin{align*} [(a,b)]\cdot[(e,f)]=[(ae+bf,af+be)] \end{align*} and \begin{align*} [(c,d)]\cdot[(e,f)]=[(ce+df,cf+de)]. \end{align*} Using this, equation (VI) becomes \begin{align*} [(ae+bf,af+be)]\preceq [(ce+df,cf+de)]. \end{align*}
Using (III) then gives us \begin{align*}\tag{VII} (ae+bf)+(cf+de)\leq (af+be)+(ce+df). \end{align*}
At this point I'm stuck again. I was hoping to somehow link equations (V) and (VII) but that doesn't seem to work out. So I assume my approach was wrong, does anyone have an idea how to make this proof work?
You want to prove (VI). Intuitively, that is $(a-b)·(e-f) \preceq (c-d)·(e-f)$. You are intuitively given $(e-f) \succ (0-0)$, which implies $e+0 > f+0$. So let $g∈ℕ$ such that $e = f+g$. You are also intuitively given $(a-b) \preceq (c-d)$, which implies $a+d ≤ b+c$. So now multiply by $g$. You get $(a+d)·g ≤ (b+c)·g$. Intuitively replace $g$ by $e-f$. You cannot literally do that since you don't have subtraction, but you can simulate it by adding the appropriate things to both sides. For example, to replace the first $g$ you add $(a+d)·f$ to both sides. Do the same for the second $g$ and you should get (VII) as desired.