Theorem fmtno

Description: The N th Fermat number. (Contributed by AV, 13-Jun-2021)

	Ref	Expression
Assertion	fmtno	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)=2^{2^N}+1$$

Proof

Step	Hyp	Ref	Expression
1		df-fmtno	$$⊢\mathrm{FermatNo}=\left(n\in {\mathbb{N}}_0⟼2^{2^n}+1\right)$$
2		oveq2	$$⊢n=N\to 2^n=2^N$$
3	2	oveq2d	$$⊢n=N\to 2^{2^n}=2^{2^N}$$
4	3	oveq1d	$$⊢n=N\to 2^{2^n}+1=2^{2^N}+1$$
5		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
6		ovexd	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}+1\in \mathrm{V}$$
7	1 4 5 6	fvmptd3	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)=2^{2^N}+1$$