Theorem gt0ne0d

Description: Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypothesis	gt0ne0d.1	⊢ ( 𝜑 → 0 < 𝐴 )
Assertion	gt0ne0d	⊢ ( 𝜑 → 𝐴 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		gt0ne0d.1	⊢ ( 𝜑 → 0 < 𝐴 )
2		0re	⊢ 0 ∈ ℝ
3		ltne	⊢ ( ( 0 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
4	2 1 3	sylancr	⊢ ( 𝜑 → 𝐴 ≠ 0 )