Description: The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | fmtnole4prm | ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4 ) → ( FermatNo ‘ 𝑁 ) ∈ ℙ ) |
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 ‘ 𝑁 ) ∈ ℙ ) |