Rules of Arithmetic and Order in an Ordered Field

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $r$, with $+$, $\cdot$, $0$, $1$ and $\le$, be an ordered field, with $<$ the strict relation of $\le$, negatives and differences as in Negatives, Differences, Reciprocals and Quotients §negative, reciprocals and quotients as in Negatives, Differences, Reciprocals and Quotients §reciprocal, and absolute values as in Absolute Value in an Ordered Field §absolute-value. Let $x,y,z,w\in r$.

¶ $0\cdot x=0$, and if $x\cdot y=0$ then $x=0$ or $y=0$.

¶ $-(-x)=x$, $-(x+y)=(-x)+(-y)$, $(-x)\cdot y=-(x\cdot y)$ and $(-x)\cdot(-y)=x\cdot y$.

¶ If $x\neq0$ and $y\neq0$, then $x\cdot y\neq0$, $(x\cdot y)^{-1}=x^{-1}\cdot y^{-1}$ and $(x^{-1})^{-1}=x$.

¶ If $x\le y$ and $z\le w$, then $x+z\le y+w$; $x<y$ if and only if $x+z<y+z$; and $x\le y$ if and only if $0\le y-x$.

¶ $x\le y$ if and only if $-y\le-x$.

¶ If $0<z$, then $x\le y$ if and only if $x\cdot z\le y\cdot z$, and $x<y$ if and only if $x\cdot z<y\cdot z$.

¶ $0\le x\cdot x$, and $0<1$.

¶ If $0<x$, then $0<x^{-1}$; if moreover $x<y$, then $y^{-1}<x^{-1}$.

¶ $0<1+1$, and if $x<y$, then $x<(x+y)/(1+1)<y$.

¶ $0\le|x|$; $|x|=0$ if and only if $x=0$; $|-x|=|x|$; $-|x|\le x\le|x|$; $|x\cdot y|=|x|\cdot|y|$; and $|x|\le y$ if and only if $-y\le x$ and $x\le y$.

¶ $|x+y|\le|x|+|y|$.