Theorem fmtnorn

Description: A Fermat number is a function value of the enumeration of the Fermat numbers. (Contributed by AV, 3-Aug-2021)

	Ref	Expression
Assertion	fmtnorn	$$⊢F\in \mathrm{ran}\mathrm{FermatNo}\leftrightarrow \exists n\in {\mathbb{N}}_0\mathrm{FermatNo}\left(n\right)=F$$

Proof

Step	Hyp	Ref	Expression
1		ovex	$$⊢2^{2^n}+1\in \mathrm{V}$$
2		df-fmtno	$$⊢\mathrm{FermatNo}=\left(n\in {\mathbb{N}}_0⟼2^{2^n}+1\right)$$
3	1 2	fnmpti	$$⊢\mathrm{FermatNo}Fn{\mathbb{N}}_0$$
4		fvelrnb	$$⊢\mathrm{FermatNo}Fn{\mathbb{N}}_0\to \left(F\in \mathrm{ran}\mathrm{FermatNo}\leftrightarrow \exists n\in {\mathbb{N}}_0\mathrm{FermatNo}\left(n\right)=F\right)$$
5	3 4	ax-mp	$$⊢F\in \mathrm{ran}\mathrm{FermatNo}\leftrightarrow \exists n\in {\mathbb{N}}_0\mathrm{FermatNo}\left(n\right)=F$$