Theorem gt0ne0i

Description: Positive means nonzero (useful for ordering theorems involving division). (Contributed by NM, 16-Sep-1999)

	Ref	Expression
Hypothesis	lt2.1	$$⊢A\in ℝ$$
Assertion	gt0ne0i	$$⊢0<A\to A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		lt2.1	$$⊢A\in ℝ$$
2		0re	$$⊢0\in ℝ$$
3	2 1	ltnei	$$⊢0<A\to A\ne 0$$