Theorem 0nrp

Description: Zero is not a positive real. Axiom 9 of Apostol p. 20. (Contributed by NM, 27-Oct-2007)

	Ref	Expression
Assertion	0nrp	$$⊢\neg 0\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2	1	ltnri	$$⊢\neg 0<0$$
3		rpgt0	$$⊢0\in {ℝ}^{+}\to 0<0$$
4	2 3	mto	$$⊢\neg 0\in {ℝ}^{+}$$