Definition df-fmtno

Description: Define the function that enumerates theFermat numbers, see definition in ApostolNT p. 7. (Contributed by AV, 13-Jun-2021)

	Ref	Expression
Assertion	df-fmtno	⊢ FermatNo = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfmtno	⊢ FermatNo
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		c2	⊢ 2
4		cexp	⊢ ↑
5	1	cv	⊢ 𝑛
6	3 5 4	co	⊢ ( 2 ↑ 𝑛 )
7	3 6 4	co	⊢ ( 2 ↑ ( 2 ↑ 𝑛 ) )
8		caddc	⊢ +
9		c1	⊢ 1
10	7 9 8	co	⊢ ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 )
11	1 2 10	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )
12	0 11	wceq	⊢ FermatNo = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )