Square of Non-Zero Element of Ordered Integral Domain is Strictly Positive
Theorem
Let $\struct {D, +, \times, \le}$ be an ordered integral domain whose zero is $0_D$.
Then:
- $\forall x \in D: x \ne 0_D \iff \map P {x \times x}$
where $\map P {x \times x}$ denotes that $x \times x$ has the (strict) positivity property.
That is, the square of any element of an ordered integral domain is (strictly) positive if and only if that element is non-zero.
Proof
Let $x = 0_D$.
Then $x \times x = 0_D \times 0_D = 0_D$ by the properties of the ring zero.
Thus by definition of strict positivity property:
- $\neg \map P {0_D \times 0_D}$
$\Box$
Now suppose $x \ne 0_D$.
One of two cases applies:
- $\map P x$
- $\neg \map P x$
Let $\map P x$.
Then by definition of (strict) positivity:
- $\map P {x \times x}$
Now suppose $\neg \map P x$.
Then by the trichotomy law of ordered integral domains:
- $\map P {-x}$
Then again by definition:
- $\map P {\paren {-x} \times \paren {-x} }$.
But by Product of Ring Negatives:
- $\paren {-x} \times \paren {-x} = x \times x$
So again:
- $\map P {x \times x}$
Hence the result.
$\blacksquare$
Sources
- 1969: C.R.J. Clapham: Introduction to Abstract Algebra ... (previous) ... (next): Chapter $2$: Ordered and Well-Ordered Integral Domains: $\S 7$. Order: Theorem $7 \ \text{(i)}$