Metamath Proof Explorer


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=n022n+1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfmtno classFermatNo
1 vn setvarn
2 cn0 class0
3 c2 class2
4 cexp class^
5 1 cv setvarn
6 3 5 4 co class2n
7 3 6 4 co class22n
8 caddc class+
9 c1 class1
10 7 9 8 co class22n+1
11 1 2 10 cmpt classn022n+1
12 0 11 wceq wffFermatNo=n022n+1