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 ( 𝑁 ∈ ( 0 ... 4 ) → ( FermatNo ‘ 𝑁 ) ∈ ℙ )

Proof

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