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 N0FermatNoN

Proof

Step Hyp Ref Expression
1 fmtnoge3 N0FermatNoN3
2 uzuzle23 FermatNoN3FermatNoN2
3 eluz2nn FermatNoN2FermatNoN
4 1 2 3 3syl N0FermatNoN