Metamath Proof Explorer

Theorem fmtnonn

Description: Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021) (Proof shortened by AV, 4-Aug-2021)

Ref Expression
Assertion fmtnonn 
|- ( N e. NN0 -> ( FermatNo ` N ) e. NN )

Proof

Step Hyp Ref Expression
1 fmtnoge3 
 |-  ( N e. NN0 -> ( FermatNo ` N ) e. ( ZZ>= ` 3 ) )
2 uzuzle23 
 |-  ( ( FermatNo ` N ) e. ( ZZ>= ` 3 ) -> ( FermatNo ` N ) e. ( ZZ>= ` 2 ) )
3 eluz2nn 
 |-  ( ( FermatNo ` N ) e. ( ZZ>= ` 2 ) -> ( FermatNo ` N ) e. NN )
4 1 2 3 3syl 
 |-  ( N e. NN0 -> ( FermatNo ` N ) e. NN )