How do I prove that in totally ordered fields $(f_1\,{\preceq}\,f_2)\,{\land}\,0_F\,{\preceq}\,f_3{\implies}f_1f_3\,{\preceq}\,f_2f_3$ is true?
I am pretty sure I've seen this theorem used, although during a search on the Internet I still couldn't find any proof of it.
Let me recall from Wikipedia that:
Suppose that $f_1\preceq f_2$ and $0_F\preceq f_3$.
By i) we have $$0_F=f_1-f_1 \preceq f_2-f_1$$
By ii) we have $$0_F=0_F\cdot f_3 \preceq (f_2-f_1)\cdot f_3=f_2\cdot f_3- f_1\cdot f_3$$
By i) we have $$f_1\cdot f_3 =0_F+f_1\cdot f_3 \preceq f_2\cdot f_3- f_1\cdot f_3+f_1\cdot f_3 =f_2\cdot f_3$$