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 ) e. Prime

Proof

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