Let $(K, +, \cdot, >)$ be an ordered Field and $x,y,x',y' \in K$. Conclude from the ordered Field axioms (O1) - (O3) that:
$$ 0 \leq x < y \wedge 0 \leq x' < y' \implies 0 \leq xx'< yy' $$
Justify each single step.
The ordered field axioms in my course are given as: $$1: \text{For all }x \in K \text{, exactly one of those properties applies: } x > 0, x = 0, -x > 0$$ $$2: x > 0 \wedge y > 0 \implies x + y > 0, x,y \in K$$ $$3: x > 0 \wedge y > 0 \implies x \cdot y > 0, x,y \in K$$
My attempt:
We multiply $0 \leq x < y$ by $y'$ from the right. This gives $$0 \leq xy' < yy'$$
We also multiply $0 \leq x' < y'$ by $x$ from the left. This gives $$0 \leq xx' < xy'$$
Using axiom 3, we see that $$0 \leq xx' < xy'< yy'$$
So we can see that $$0 \leq xx' < yy'$$
Is this correct ? This seems a bit too straightforward, so I'm especially unsure. Do we only need to use axiom 3 and 1 ? Is axiom 2 not needed ?
As for your proof, it is correct, but you were using property not stated in the axioms. Namely multiplying both sides of the equality, i.e.
$$(a<b \wedge c>0)\implies ac<bc$$
To prove this you proceed as follows:
The proof looks fine except in points 2 and 6 it relies on monotonicity, i.e. the following property:
$$ a<b \implies a+c<b+c$$
This property is usually assumed as one of the axioms of the ordered field. In your case it is not. Moreover, I believe that in fact it can't be proved from axioms 1-3.
To see this, consider any ordered field $K$ in the usual sense ($\mathbb R$ or $\mathbb Q$ will do) and take any (linear) order $<_+$ on the set $(0,\infty)$ and any (linear) order $<_-$ on the set $(-\infty, 0)$. Now define a new order $<^*$ in such a way that $x<^*y$ iff one of the following condition holds.
Then $<^*$ is a linear order on $K$, axioms 1-3 hold but $<_+$ and $<_-$ can be chosen in such a way that monotonicity fails.