Metamath Proof Explorer

Theorem fmtno0prm

Description: The 0 th Fermat number is a prime (_first Fermat prime_). (Contributed by AV, 13-Jun-2021)

Ref Expression
Assertion fmtno0prm 
|- ( FermatNo ` 0 ) e. Prime

Proof

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