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 
|- ( FermatNo ` 2 ) e. Prime

Proof

Step Hyp Ref Expression
1 fmtno2 
 |-  ( FermatNo ` 2 ) = ; 1 7
2 17prm 
 |-  ; 1 7 e. Prime
3 1 2 eqeltri 
 |-  ( FermatNo ` 2 ) e. Prime