Theorem nnne0ALT

Description: Alternate version of nnne0 . A positive integer is nonzero. (Contributed by NM, 27-Sep-1999) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	nnne0ALT	⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		0nnnALT	⊢ ¬ 0 ∈ ℕ
2		eleq1	⊢ ( 𝐴 = 0 → ( 𝐴 ∈ ℕ ↔ 0 ∈ ℕ ) )
3	1 2	mtbiri	⊢ ( 𝐴 = 0 → ¬ 𝐴 ∈ ℕ )
4	3	necon2ai	⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )