Theorem 0nnn

Description: Zero is not a positive integer. (Contributed by NM, 25-Aug-1999) Remove dependency on ax-pre-mulgt0 . (Revised by Steven Nguyen, 30-Jan-2023)

	Ref	Expression
Assertion	0nnn	⊢ ¬ 0 ∈ ℕ

Proof

Step	Hyp	Ref	Expression
1		neirr	⊢ ¬ 0 ≠ 0
2		nnne0	⊢ ( 0 ∈ ℕ → 0 ≠ 0 )
3	1 2	mto	⊢ ¬ 0 ∈ ℕ