Metamath Proof Explorer


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 ‘ 𝑁 ) ∈ ℙ )