Definition df-fmtno 41440

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 = ( n e. NN0 |-> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )

Detailed syntax breakdown of Definition df-fmtno

Step	Hyp	Ref	Expression
1		cfmtno 41439	. 2 class FermatNo
2		vn	. . 3 setvar n
3		cn0 11292	. . 3 class NN0
4		c2 11070	. . . . 5 class 2
5	2	cv 1482	. . . . . 6 class n
6		cexp 12860	. . . . . 6 class ^
7	4, 5, 6	co 6650	. . . . 5 class ( 2 ^ n )
8	4, 7, 6	co 6650	. . . 4 class ( 2 ^ ( 2 ^ n ) )
9		c1 9937	. . . 4 class 1
10		caddc 9939	. . . 4 class +
11	8, 9, 10	co 6650	. . 3 class ( ( 2 ^ ( 2 ^ n ) ) + 1 )
12	2, 3, 11	cmpt 4729	. 2 class ( n e. NN0 |-> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
13	1, 12	wceq 1483	1 wff FermatNo = ( n e. NN0 |-> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )

This definition is referenced by:  fmtno  41441  fmtnorn  41446  fmtnof1  41447  fmtnodvds  41456