Theorem nnne0i

Description: A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999)

	Ref	Expression
Hypothesis	nngt0.1	$$⊢A\in \mathbb{N}$$
Assertion	nnne0i	$$⊢A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		nngt0.1	$$⊢A\in \mathbb{N}$$
2	1	nnrei	$$⊢A\in ℝ$$
3	1	nngt0i	$$⊢0<A$$
4	2 3	gt0ne0ii	$$⊢A\ne 0$$