Theorem fmtno

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

	Ref	Expression
Assertion	fmtno	⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		df-fmtno	⊢ FermatNo = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )
2		oveq2	⊢ ( 𝑛 = 𝑁 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑁 ) )
3	2	oveq2d	⊢ ( 𝑛 = 𝑁 → ( 2 ↑ ( 2 ↑ 𝑛 ) ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
4	3	oveq1d	⊢ ( 𝑛 = 𝑁 → ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
5		id	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
6		ovexd	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ∈ V )
7	1 4 5 6	fvmptd3	⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )