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 ∈ ℙ