Metamath Proof Explorer

Theorem fmtnofz04prm

Description: The first five Fermat numbers are prime, see remark in ApostolNT p. 7. (Contributed by AV, 28-Jul-2021)

Ref Expression
Assertion fmtnofz04prm ⊢ N ∈ 0 … 4 → FermatNo ⁡ N ∈ ℙ

Proof

Step Hyp Ref Expression
1 4nn0 ⊢ 4 ∈ ℕ 0
2 el1fzopredsuc ⊢ 4 ∈ ℕ 0 → N ∈ 0 … 4 ↔ N = 0 ∨ N ∈ 1 ..^ 4 ∨ N = 4
3 1 2 ax-mp ⊢ N ∈ 0 … 4 ↔ N = 0 ∨ N ∈ 1 ..^ 4 ∨ N = 4
4 fveq2 ⊢ N = 0 → FermatNo ⁡ N = FermatNo ⁡ 0
5 fmtno0prm ⊢ FermatNo ⁡ 0 ∈ ℙ
6 4 5 eqeltrdi ⊢ N = 0 → FermatNo ⁡ N ∈ ℙ
7 eltpi ⊢ N ∈ 1 2 3 → N = 1 ∨ N = 2 ∨ N = 3
8 fveq2 ⊢ N = 1 → FermatNo ⁡ N = FermatNo ⁡ 1
9 fmtno1prm ⊢ FermatNo ⁡ 1 ∈ ℙ
10 8 9 eqeltrdi ⊢ N = 1 → FermatNo ⁡ N ∈ ℙ
11 fveq2 ⊢ N = 2 → FermatNo ⁡ N = FermatNo ⁡ 2
12 fmtno2prm ⊢ FermatNo ⁡ 2 ∈ ℙ
13 11 12 eqeltrdi ⊢ N = 2 → FermatNo ⁡ N ∈ ℙ
14 fveq2 ⊢ N = 3 → FermatNo ⁡ N = FermatNo ⁡ 3
15 fmtno3prm ⊢ FermatNo ⁡ 3 ∈ ℙ
16 14 15 eqeltrdi ⊢ N = 3 → FermatNo ⁡ N ∈ ℙ
17 10 13 16 3jaoi ⊢ N = 1 ∨ N = 2 ∨ N = 3 → FermatNo ⁡ N ∈ ℙ
18 7 17 syl ⊢ N ∈ 1 2 3 → FermatNo ⁡ N ∈ ℙ
19 fzo1to4tp ⊢ 1 ..^ 4 = 1 2 3
20 18 19 eleq2s ⊢ N ∈ 1 ..^ 4 → FermatNo ⁡ N ∈ ℙ
21 fveq2 ⊢ N = 4 → FermatNo ⁡ N = FermatNo ⁡ 4
22 fmtno4prm ⊢ FermatNo ⁡ 4 ∈ ℙ
23 21 22 eqeltrdi ⊢ N = 4 → FermatNo ⁡ N ∈ ℙ
24 6 20 23 3jaoi ⊢ N = 0 ∨ N ∈ 1 ..^ 4 ∨ N = 4 → FermatNo ⁡ N ∈ ℙ
25 3 24 sylbi ⊢ N ∈ 0 … 4 → FermatNo ⁡ N ∈ ℙ