Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fmtno Structured version   Visualization version   GIF version

Definition df-fmtno 46196
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
StepHypRef Expression
1 cfmtno 46195 . 2 class FermatNo
2 vn . . 3 setvar 𝑛
3 cn0 12472 . . 3 class 0
4 c2 12267 . . . . 5 class 2
52cv 1541 . . . . . 6 class 𝑛
6 cexp 14027 . . . . . 6 class
74, 5, 6co 7409 . . . . 5 class (2↑𝑛)
84, 7, 6co 7409 . . . 4 class (2↑(2↑𝑛))
9 c1 11111 . . . 4 class 1
10 caddc 11113 . . . 4 class +
118, 9, 10co 7409 . . 3 class ((2↑(2↑𝑛)) + 1)
122, 3, 11cmpt 5232 . 2 class (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1))
131, 12wceq 1542 1 wff FermatNo = (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1))
Colors of variables: wff setvar class
This definition is referenced by:  fmtno  46197  fmtnorn  46202  fmtnof1  46203  fmtnodvds  46212
  Copyright terms: Public domain W3C validator