Metamath Proof Explorer

Theorem rpne0

Description: A positive real is nonzero. (Contributed by NM, 18-Jul-2008)

		Ref	Expression
	Assertion	rpne0	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		rpregt0	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
2		gt0ne0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ≠ 0 )