Theorem fmtnonn

Description: Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021) (Proof shortened by AV, 4-Aug-2021)

	Ref	Expression
Assertion	fmtnonn	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		fmtnoge3	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)\in {\mathbb{Z}}_{\ge 3}$$
2		uzuzle23	$$⊢\mathrm{FermatNo}\left(N\right)\in {\mathbb{Z}}_{\ge 3}\to \mathrm{FermatNo}\left(N\right)\in {\mathbb{Z}}_{\ge 2}$$
3		eluz2nn	$$⊢\mathrm{FermatNo}\left(N\right)\in {\mathbb{Z}}_{\ge 2}\to \mathrm{FermatNo}\left(N\right)\in \mathbb{N}$$
4	1 2 3	3syl	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)\in \mathbb{N}$$