Theorem fmtnole4prm

Description: The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021)

	Ref	Expression
Assertion	fmtnole4prm	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4 ) → ( FermatNo ‘ 𝑁 ) ∈ ℙ )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4 ) → 𝑁 ∈ ℕ0 )
2		4nn0	⊢ 4 ∈ ℕ0
3	2	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4 ) → 4 ∈ ℕ0 )
4		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4 ) → 𝑁 ≤ 4 )
5		elfz2nn0	⊢ ( 𝑁 ∈ ( 0 ... 4 ) ↔ ( 𝑁 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 𝑁 ≤ 4 ) )
6	1 3 4 5	syl3anbrc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4 ) → 𝑁 ∈ ( 0 ... 4 ) )
7		fmtnofz04prm	⊢ ( 𝑁 ∈ ( 0 ... 4 ) → ( FermatNo ‘ 𝑁 ) ∈ ℙ )
8	6 7	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4 ) → ( FermatNo ‘ 𝑁 ) ∈ ℙ )