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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfmtno	|- FermatNo
1		vn	|- n
2		cn0	|- NN0
3		c2	|- 2
4		cexp	|- ^
5	1	cv	|- n
6	3 5 4	co	|- ( 2 ^ n )
7	3 6 4	co	|- ( 2 ^ ( 2 ^ n ) )
8		caddc	|- +
9		c1	|- 1
10	7 9 8	co	|- ( ( 2 ^ ( 2 ^ n ) ) + 1 )
11	1 2 10	cmpt	|- ( n e. NN0 |-> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
12	0 11	wceq	|- FermatNo = ( n e. NN0 |-> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )