Theorem: Properties of Ordered Field

Let $\struct {F, +, \cdot}$ be an ordered field with unity $1$, zero $0$.
Denote the strict order by $<$ and the weak order by $\le$.
Let $\Char F$ denote the characteristic of $F$.
Then the following hold for all $x, y, z \in F$:
:$(1): \quad x < 0 \iff -x > 0$
:$(2): \quad x > y \iff x - y > 0$
:$(3): \quad x < y \iff -x > -y$
:$(4): \quad \paren {z < 0} \land \paren {x < y} \implies x z > y z$
:$(5): \quad x \ne 0 \implies x^2 > 0$
:$(6): \quad 1 > 0$
:$(7): \quad \Char F = 0$
:$(8): \quad x > y > 0 \iff y^{-1} > x^{-1} > 0$

Proof:
By definition of ordering, the relation $\le$ is:
:reflexive
:transitive
:antisymmetric
and furthermore, every pair of elements is comparable.
The order is compatible with $F$ in the sense that, for all $x, y, z, c \in F$:
:$x < y \implies x + z < y + z$
:$c > 0,\ x < y \implies c x < c y$
The proof is by repeated deduction from these properties.
* $(1): \quad x < 0 \iff -x > 0$:
{{begin-eqn}}
{{eqn | l = x
      | o = <
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = x - x
      | o = <
      | r = 0 - x
}}
{{eqn | ll= \leadsto
      | l = -x
      | o = >
      | r = 0
}}
{{end-eqn}}
Conversely:
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = x - x
      | o = >
      | r = 0 - x
}}
{{eqn | ll= \leadsto
      | l = -x
      | o = <
      | r = 0
}}
{{end-eqn}}
* $(2): \quad x > y \iff x - y > 0$:
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = y
}}
{{eqn | ll= \leadsto
      | l = x - y
      | o = >
      | r = y - y = 0
}}
{{end-eqn}}
Conversely:
{{begin-eqn}}
{{eqn | l = x - y > 0
      | o = >
      | r = y
}}
{{eqn | ll= \leadsto
      | l = x - y + y
      | o = >
      | r = y
}}
{{eqn | ll= \leadsto
      | l = x
      | o = >
      | r = y
}}
{{end-eqn}}
* $(3): \quad x < y \iff -x > -y$:
{{begin-eqn}}
{{eqn | l = x
      | o = <
      | r = y
}}
{{eqn | ll= \leadsto
      | l = x - x - y
      | o = <
      | r = y - x - y
}}
{{eqn | ll= \leadsto
      | l = -y
      | o = <
      | r = -x
}}
{{end-eqn}}
Conversely:
{{begin-eqn}}
{{eqn | l = -y
      | o = <
      | r = -x
}}
{{eqn | ll= \leadsto
      | l = -y + y + x
      | o = <
      | r = -x + y + x
}}
{{eqn | ll= \leadsto
      | l = x
      | o = <
      | r = y
}}
{{end-eqn}}
* $(4): \quad (z < 0) \land (x < y) \implies x z > y z$:
By parts 1 and 3 above, if $z < 0$, $x < y$ then $-z > 0$ and $-x > -y$.
Then:
:$x z = \paren {-x} \paren {-z} > \paren {-y} \paren {-z} = y z$
* $(5): \quad x \ne 0 \implies x^2 > 0$:
If $x > 0$, then:
:$x^2 = x \cdot x > x \cdot 0 = 0$
If $x < 0$, then by 1, $-x > 0$, so:
:$x^2 = \paren {-x} \cdot \paren {-x} > \paren {-x} \cdot 0 = 0$
* $(6): \quad 1 > 0$:
This is immediate from $(5)$, noting that $1 = 1^2$ is a square.
* $(7): \quad \Char F = 0$:
By $(6)$, we have:
:$0 < 1 < 1 + 1 < 1 + 1 + 1 < \cdots$
so $n \cdot 1 \ne 0$ for all $n \in \N$.
* $(8): \quad x > y > 0 \iff y^{-1} > x^{-1} > 0$:
First let $x > 0$.
{{AimForCont}} $x^{-1} < 0$.
Then by $(4)$:
:$0 = 0 \cdot x^{-1} > x \cdot x^{-1} = 1$
which contradicts $(6)$, so $x^{-1} > 0$.
Now let $x > y > 0$.
Then:
{{begin-eqn}}
{{eqn | l = x^{-1} y^{-1} x
      | o = >
      | r = x^{-1} y^{-1} y > 0
}}
{{eqn | ll= \leadsto
      | l = y^{-1}
      | o = >
      | r = x^{-1} > 0
}}
{{end-eqn}}
The converse follows upon interchanging $x^{-1} \leftrightarrow x$ and $y^{-1} \leftrightarrow y$.
{{qed}}
Category:Ordered Fields
4z5mk8shpveswkbwabq5lz0n6miro39