Theorem gt0ne0

Description: Positive implies nonzero. (Contributed by NM, 3-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	gt0ne0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		0red	⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
2		ltne	⊢ ( ( 0 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
3	1 2	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )