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

Proof

Step	Hyp	Ref	Expression
1		fmtno4	⊢ ( FermatNo ‘ 4 ) = ; ; ; ; 6 5 5 3 7
2		fmtno4prm	⊢ ( FermatNo ‘ 4 ) ∈ ℙ
3	1 2	eqeltrri	⊢ ; ; ; ; 6 5 5 3 7 ∈ ℙ