Totally Ordered Ring Zero Precedes Element or its Inverse

Theorem

Let $\struct {R, +, \circ, \preceq}$ be an ordered ring.

From the definition of ordered ring, $\preceq$ is compatible with $+$.

Let $0_R$ be the zero element of $R$.

Let $x \ne 0_R$ be a non-zero element of $R$.

Let $-x$ be the ring negative of $x$.

Then:

$0_R \prec x \lor 0_R \prec -x$

but not both.

By the definition of total ordering, $\preceq$ is connected.

As $x \ne 0_R$, one of the following is true, but not both:

$(1): \quad 0_R \prec x$

$(2): \quad x \prec 0_R$

If $(2)$, because $\prec$ is compatible with $+$:

$\ds x$

$\prec$

$\ds 0_R$

$\ds \leadsto \ \ $

$\ds x + \paren {-x}$

$\prec$

$\ds 0_R + \paren {-x}$

$\ds \leadsto \ \ $

$\ds 0_R$

$\prec$

$\ds -x$

Definition of Ring Zero, Definition of Ring Negative

$\blacksquare$