Theorem fmtno1prm

Description: The 1 st Fermat number is a prime (_second Fermat prime_). (Contributed by AV, 13-Jun-2021)

	Ref	Expression
Assertion	fmtno1prm	⊢ ( FermatNo ‘ 1 ) ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		fmtno1	⊢ ( FermatNo ‘ 1 ) = 5
2		5prm	⊢ 5 ∈ ℙ
3	1 2	eqeltri	⊢ ( FermatNo ‘ 1 ) ∈ ℙ