This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ ℝ⁺

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