Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Number theory (extension)
Fermat numbers
65537prm
Next ⟩
fmtnofz04prm
Metamath Proof Explorer
Ascii
Unicode
Theorem
65537prm
Description:
65537 is a prime number (the
fifth Fermat prime
).
(Contributed by
AV
, 28-Jul-2021)
Ref
Expression
Assertion
65537prm
⊢
65537
∈
ℙ
Proof
Step
Hyp
Ref
Expression
1
fmtno4
⊢
FermatNo
⁡
4
=
65537
2
fmtno4prm
⊢
FermatNo
⁡
4
∈
ℙ
3
1
2
eqeltrri
⊢
65537
∈
ℙ