Metamath Proof Explorer

Theorem fmtno1prm

Description: The 1 st Fermat number is a prime (_second Fermat prime_). (Contributed by AV, 13-Jun-2021)

Ref Expression
Assertion fmtno1prm 
|- ( FermatNo ` 1 ) e. Prime

Proof

Step Hyp Ref Expression
1 fmtno1 
 |-  ( FermatNo ` 1 ) = 5
2 5prm 
 |-  5 e. Prime
3 1 2 eqeltri 
 |-  ( FermatNo ` 1 ) e. Prime