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	⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		fmtnoge3	⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 3 ) )
2		uzuzle23	⊢ ( ( FermatNo ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 3 ) → ( FermatNo ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) )
3		eluz2nn	⊢ ( ( FermatNo ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) → ( FermatNo ‘ 𝑁 ) ∈ ℕ )
4	1 2 3	3syl	⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℕ )