Theorem fmtno0prm

Description: The 0 th Fermat number is a prime (_first Fermat prime_). (Contributed by AV, 13-Jun-2021)

	Ref	Expression
Assertion	fmtno0prm	⊢ ( FermatNo ‘ 0 ) ∈ ℙ

Proof

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