Definition df-fmtno 44868

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

Assertion

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

Detailed syntax breakdown of Definition df-fmtno

Step	Hyp	Ref	Expression
1		cfmtno 44867	. 2 class FermatNo
2		vn	. . 3 setvar 𝑛
3		cn0 12163	. . 3 class ℕ0
4		c2 11958	. . . . 5 class 2
5	2	cv 1538	. . . . . 6 class 𝑛
6		cexp 13710	. . . . . 6 class ↑
7	4, 5, 6	co 7255	. . . . 5 class (2↑𝑛)
8	4, 7, 6	co 7255	. . . 4 class (2↑(2↑𝑛))
9		c1 10803	. . . 4 class 1
10		caddc 10805	. . . 4 class +
11	8, 9, 10	co 7255	. . 3 class ((2↑(2↑𝑛)) + 1)
12	2, 3, 11	cmpt 5153	. 2 class (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1))
13	1, 12	wceq 1539	1 wff FermatNo = (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1))

This definition is referenced by:  fmtno  44869  fmtnorn  44874  fmtnof1  44875  fmtnodvds  44884