Theorem fmtno2prm

Description: The 2 nd Fermat number is a prime (_third Fermat prime_). (Contributed by AV, 13-Jun-2021)

	Ref	Expression
Assertion	fmtno2prm	⊢ ( FermatNo ‘ 2 ) ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		fmtno2	⊢ ( FermatNo ‘ 2 ) = ; 1 7
2		17prm	⊢ ; 1 7 ∈ ℙ
3	1 2	eqeltri	⊢ ( FermatNo ‘ 2 ) ∈ ℙ