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	$$⊢\mathrm{FermatNo}=\left(n\in {\mathbb{N}}_0⟼2^{2^n}+1\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfmtno	$$class\mathrm{FermatNo}$$
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		c2	$$class2$$
4		cexp	$$class^$$
5	1	cv	$$setvarn$$
6	3 5 4	co	$$class{2}^n$$
7	3 6 4	co	$$class{2}^{2^n}$$
8		caddc	$$class+$$
9		c1	$$class1$$
10	7 9 8	co	$$class\left(2^{2^n}+1\right)$$
11	1 2 10	cmpt	$$class\left(n\in {\mathbb{N}}_0⟼2^{2^n}+1\right)$$
12	0 11	wceq	$$wff\mathrm{FermatNo}=\left(n\in {\mathbb{N}}_0⟼2^{2^n}+1\right)$$