Metamath Proof Explorer


Theorem fmtno2prm

Description: The 2 nd Fermat number is a prime (_third Fermat prime_). (Contributed by AV, 13-Jun-2021)

Ref Expression
Assertion fmtno2prm FermatNo2

Proof

Step Hyp Ref Expression
1 fmtno2 FermatNo2=17
2 17prm 17
3 1 2 eqeltri FermatNo2