Metamath Proof Explorer

Theorem fmtnole4prm

Description: The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021)

Ref Expression
Assertion fmtnole4prm 
|- ( ( N e. NN0 /\ N <_ 4 ) -> ( FermatNo ` N ) e. Prime )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. NN0 /\ N <_ 4 ) -> N e. NN0 )
2 4nn0 
 |-  4 e. NN0
3 2 a1i 
 |-  ( ( N e. NN0 /\ N <_ 4 ) -> 4 e. NN0 )
4 simpr 
 |-  ( ( N e. NN0 /\ N <_ 4 ) -> N <_ 4 )
5 elfz2nn0 
 |-  ( N e. ( 0 ... 4 ) <-> ( N e. NN0 /\ 4 e. NN0 /\ N <_ 4 ) )
6 1 3 4 5 syl3anbrc 
 |-  ( ( N e. NN0 /\ N <_ 4 ) -> N e. ( 0 ... 4 ) )
7 fmtnofz04prm 
 |-  ( N e. ( 0 ... 4 ) -> ( FermatNo ` N ) e. Prime )
8 6 7 syl 
 |-  ( ( N e. NN0 /\ N <_ 4 ) -> ( FermatNo ` N ) e. Prime )