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 e. ( 0 ... 4 ) -> ( FermatNo ` N ) e. Prime )

Proof

Step Hyp Ref Expression
1 4nn0 
 |-  4 e. NN0
2 el1fzopredsuc 
 |-  ( 4 e. NN0 -> ( N e. ( 0 ... 4 ) <-> ( N = 0 \/ N e. ( 1 ..^ 4 ) \/ N = 4 ) ) )
3 1 2 ax-mp 
 |-  ( N e. ( 0 ... 4 ) <-> ( N = 0 \/ N e. ( 1 ..^ 4 ) \/ N = 4 ) )
4 fveq2 
 |-  ( N = 0 -> ( FermatNo ` N ) = ( FermatNo ` 0 ) )
5 fmtno0prm 
 |-  ( FermatNo ` 0 ) e. Prime
6 4 5 eqeltrdi 
 |-  ( N = 0 -> ( FermatNo ` N ) e. Prime )
7 eltpi 
 |-  ( N e. { 1 , 2 , 3 } -> ( N = 1 \/ N = 2 \/ N = 3 ) )
8 fveq2 
 |-  ( N = 1 -> ( FermatNo ` N ) = ( FermatNo ` 1 ) )
9 fmtno1prm 
 |-  ( FermatNo ` 1 ) e. Prime
10 8 9 eqeltrdi 
 |-  ( N = 1 -> ( FermatNo ` N ) e. Prime )
11 fveq2 
 |-  ( N = 2 -> ( FermatNo ` N ) = ( FermatNo ` 2 ) )
12 fmtno2prm 
 |-  ( FermatNo ` 2 ) e. Prime
13 11 12 eqeltrdi 
 |-  ( N = 2 -> ( FermatNo ` N ) e. Prime )
14 fveq2 
 |-  ( N = 3 -> ( FermatNo ` N ) = ( FermatNo ` 3 ) )
15 fmtno3prm 
 |-  ( FermatNo ` 3 ) e. Prime
16 14 15 eqeltrdi 
 |-  ( N = 3 -> ( FermatNo ` N ) e. Prime )
17 10 13 16 3jaoi 
 |-  ( ( N = 1 \/ N = 2 \/ N = 3 ) -> ( FermatNo ` N ) e. Prime )
18 7 17 syl 
 |-  ( N e. { 1 , 2 , 3 } -> ( FermatNo ` N ) e. Prime )
19 fzo1to4tp 
 |-  ( 1 ..^ 4 ) = { 1 , 2 , 3 }
20 18 19 eleq2s 
 |-  ( N e. ( 1 ..^ 4 ) -> ( FermatNo ` N ) e. Prime )
21 fveq2 
 |-  ( N = 4 -> ( FermatNo ` N ) = ( FermatNo ` 4 ) )
22 fmtno4prm 
 |-  ( FermatNo ` 4 ) e. Prime
23 21 22 eqeltrdi 
 |-  ( N = 4 -> ( FermatNo ` N ) e. Prime )
24 6 20 23 3jaoi 
 |-  ( ( N = 0 \/ N e. ( 1 ..^ 4 ) \/ N = 4 ) -> ( FermatNo ` N ) e. Prime )
25 3 24 sylbi 
 |-  ( N e. ( 0 ... 4 ) -> ( FermatNo ` N ) e. Prime )