Theorem fmtno3prm

Description: The 3 rd Fermat number is a prime (_fourth Fermat prime_). (Contributed by AV, 15-Jun-2021)

	Ref	Expression
Assertion	fmtno3prm	⊢ ( FermatNo ‘ 3 ) ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		fmtno3	⊢ ( FermatNo ‘ 3 ) = ; ; 2 5 7
2		257prm	⊢ ; ; 2 5 7 ∈ ℙ
3	1 2	eqeltri	⊢ ( FermatNo ‘ 3 ) ∈ ℙ