Metamath Proof Explorer


Theorem fmtno3prm

Description: The 3 rd Fermat number is a prime (_fourth Fermat prime_). (Contributed by AV, 15-Jun-2021)

Ref Expression
Assertion fmtno3prm FermatNo 3

Proof

Step Hyp Ref Expression
1 fmtno3 FermatNo 3 = 257
2 257prm 257
3 1 2 eqeltri FermatNo 3