Real Number is Greater than Zero iff its Negative is Less than Zero

From ProofWiki
Jump to navigation Jump to search

Theorem

$\forall x \in \R: x > 0 \iff \paren {-x} < 0$


Proof

Let $x > 0$.

\(\ds x\) \(>\) \(\ds 0\)
\(\ds \leadsto \ \ \) \(\ds x + \paren {-x}\) \(>\) \(\ds 0 + \paren {-x}\) Real Number Axiom $\R \text O2$: Usual Ordering is Compatible with Multiplication
\(\ds \leadsto \ \ \) \(\ds 0\) \(>\) \(\ds 0 + \paren {-x}\) Real Number Axiom $\R \text A4$: Inverses for Addition
\(\ds \leadsto \ \ \) \(\ds 0\) \(>\) \(\ds \paren {-x}\) Real Number Axiom $\R \text A3$: Identity for Addition

$\Box$


Let $\paren {-x} < 0$.

\(\ds \paren {-x}\) \(<\) \(\ds 0\)
\(\ds \leadsto \ \ \) \(\ds x + \paren {-x}\) \(<\) \(\ds x + 0\) Real Number Axiom $\R \text O2$: Usual Ordering is Compatible with Multiplication
\(\ds \leadsto \ \ \) \(\ds 0\) \(<\) \(\ds x + 0\) Real Number Axiom $\R \text A4$: Inverses for Addition
\(\ds \leadsto \ \ \) \(\ds 0\) \(<\) \(\ds x\) Real Number Axiom $\R \text A3$: Identity for Addition

$\blacksquare$


Sources