Metamath Proof Explorer

Theorem 65537prm

Description: 65537 is a prime number (thefifth Fermat prime). (Contributed by AV, 28-Jul-2021)

Ref Expression
Assertion 65537prm 
|- ; ; ; ; 6 5 5 3 7 e. Prime

Proof

Step Hyp Ref Expression
1 fmtno4 
 |-  ( FermatNo ` 4 ) = ; ; ; ; 6 5 5 3 7
2 fmtno4prm 
 |-  ( FermatNo ` 4 ) e. Prime
3 1 2 eqeltrri 
 |-  ; ; ; ; 6 5 5 3 7 e. Prime