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	⊢ ¬ 0 ∈ ℝ+

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2	1	ltnri	⊢ ¬ 0 < 0
3		rpgt0	⊢ ( 0 ∈ ℝ+ → 0 < 0 )
4	2 3	mto	⊢ ¬ 0 ∈ ℝ+