Metamath Proof Explorer


Theorem 65537prm

Description: 65537 is a prime number (thefifth Fermat prime). (Contributed by AV, 28-Jul-2021)

Ref Expression
Assertion 65537prm 65537

Proof

Step Hyp Ref Expression
1 fmtno4 FermatNo 4 = 65537
2 fmtno4prm FermatNo 4
3 1 2 eqeltrri 65537