Strict Negativity is equivalent to Strictly Preceding Zero

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {D, +, \times}$ be an ordered integral domain, whose (strict) positivity property is denoted $P$.

Let $\le$ be the total ordering induced by $P$, and let $<$ be its strict total ordering counterpart.


Let $N$ be the (strict) negativity property on $D$:

$\forall a \in D: \map N a \iff \map P {-a}$


Then for all $a \in D$:

$\map N a \iff a < 0$


Proof

\(\ds \map N a\) \(\leadstoandfrom\) \(\ds \map P {-a}\) Definition of Strict Negativity Property
\(\ds \) \(\leadstoandfrom\) \(\ds \map P {-a + 0}\)
\(\ds \) \(\leadstoandfrom\) \(\ds a < 0\) Strict Positivity Property induces Total Ordering

$\blacksquare$


Sources