Theorem nnnfi

Description: The set of positive integers is infinite. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	nnnfi	$$⊢\neg \mathbb{N}\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
3	2	uzinf	$$⊢1\in \mathbb{Z}\to \neg \mathbb{N}\in \mathrm{Fin}$$
4	1 3	ax-mp	$$⊢\neg \mathbb{N}\in \mathrm{Fin}$$