Detailed syntax breakdown of Definition df-bpoly
| Step | Hyp | Ref
| Expression |
| 1 | | cbp 16082 |
. 2
class
BernPoly |
| 2 | | vm |
. . 3
setvar 𝑚 |
| 3 | | vx |
. . 3
setvar 𝑥 |
| 4 | | cn0 12526 |
. . 3
class
ℕ0 |
| 5 | | cc 11153 |
. . 3
class
ℂ |
| 6 | 2 | cv 1539 |
. . . 4
class 𝑚 |
| 7 | | clt 11295 |
. . . . 5
class
< |
| 8 | | vg |
. . . . . 6
setvar 𝑔 |
| 9 | | cvv 3480 |
. . . . . 6
class
V |
| 10 | | vn |
. . . . . . 7
setvar 𝑛 |
| 11 | 8 | cv 1539 |
. . . . . . . . 9
class 𝑔 |
| 12 | 11 | cdm 5685 |
. . . . . . . 8
class dom 𝑔 |
| 13 | | chash 14369 |
. . . . . . . 8
class
♯ |
| 14 | 12, 13 | cfv 6561 |
. . . . . . 7
class
(♯‘dom 𝑔) |
| 15 | 3 | cv 1539 |
. . . . . . . . 9
class 𝑥 |
| 16 | 10 | cv 1539 |
. . . . . . . . 9
class 𝑛 |
| 17 | | cexp 14102 |
. . . . . . . . 9
class
↑ |
| 18 | 15, 16, 17 | co 7431 |
. . . . . . . 8
class (𝑥↑𝑛) |
| 19 | | vk |
. . . . . . . . . . . 12
setvar 𝑘 |
| 20 | 19 | cv 1539 |
. . . . . . . . . . 11
class 𝑘 |
| 21 | | cbc 14341 |
. . . . . . . . . . 11
class
C |
| 22 | 16, 20, 21 | co 7431 |
. . . . . . . . . 10
class (𝑛C𝑘) |
| 23 | 20, 11 | cfv 6561 |
. . . . . . . . . . 11
class (𝑔‘𝑘) |
| 24 | | cmin 11492 |
. . . . . . . . . . . . 13
class
− |
| 25 | 16, 20, 24 | co 7431 |
. . . . . . . . . . . 12
class (𝑛 − 𝑘) |
| 26 | | c1 11156 |
. . . . . . . . . . . 12
class
1 |
| 27 | | caddc 11158 |
. . . . . . . . . . . 12
class
+ |
| 28 | 25, 26, 27 | co 7431 |
. . . . . . . . . . 11
class ((𝑛 − 𝑘) + 1) |
| 29 | | cdiv 11920 |
. . . . . . . . . . 11
class
/ |
| 30 | 23, 28, 29 | co 7431 |
. . . . . . . . . 10
class ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)) |
| 31 | | cmul 11160 |
. . . . . . . . . 10
class
· |
| 32 | 22, 30, 31 | co 7431 |
. . . . . . . . 9
class ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) |
| 33 | 12, 32, 19 | csu 15722 |
. . . . . . . 8
class
Σ𝑘 ∈ dom
𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) |
| 34 | 18, 33, 24 | co 7431 |
. . . . . . 7
class ((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
| 35 | 10, 14, 34 | csb 3899 |
. . . . . 6
class
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
| 36 | 8, 9, 35 | cmpt 5225 |
. . . . 5
class (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
| 37 | 4, 7, 36 | cwrecs 8336 |
. . . 4
class wrecs(
< , ℕ0, (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) |
| 38 | 6, 37 | cfv 6561 |
. . 3
class (wrecs(
< , ℕ0, (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) |
| 39 | 2, 3, 4, 5, 38 | cmpo 7433 |
. 2
class (𝑚 ∈ ℕ0,
𝑥 ∈ ℂ ↦
(wrecs( < , ℕ0, (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚)) |
| 40 | 1, 39 | wceq 1540 |
1
wff BernPoly =
(𝑚 ∈
ℕ0, 𝑥
∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚)) |