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∈123→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∈123→FermatNo⁡N∈ℙ
19 fzo1to4tp ⊢1..^4=123
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∈ℙ