Theorem 65537prm

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

	Ref	Expression
Assertion	65537prm	$$⊢65537\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		fmtno4	$$⊢\mathrm{FermatNo}\left(4\right)=65537$$
2		fmtno4prm	$$⊢\mathrm{FermatNo}\left(4\right)\in \mathbb{P}$$
3	1 2	eqeltrri	$$⊢65537\in \mathbb{P}$$