Detailed syntax breakdown of Definition df-fwddifn
Step | Hyp | Ref
| Expression |
1 | | cfwddifn 31437 |
. 2
class
△n |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | cn0 11169 |
. . 3
class
ℕ0 |
5 | | cc 9813 |
. . . 4
class
ℂ |
6 | | cpm 7745 |
. . . 4
class
↑pm |
7 | 5, 5, 6 | co 6549 |
. . 3
class (ℂ
↑pm ℂ) |
8 | | vx |
. . . 4
setvar 𝑥 |
9 | | vy |
. . . . . . . . 9
setvar 𝑦 |
10 | 9 | cv 1474 |
. . . . . . . 8
class 𝑦 |
11 | | vk |
. . . . . . . . 9
setvar 𝑘 |
12 | 11 | cv 1474 |
. . . . . . . 8
class 𝑘 |
13 | | caddc 9818 |
. . . . . . . 8
class
+ |
14 | 10, 12, 13 | co 6549 |
. . . . . . 7
class (𝑦 + 𝑘) |
15 | 3 | cv 1474 |
. . . . . . . 8
class 𝑓 |
16 | 15 | cdm 5038 |
. . . . . . 7
class dom 𝑓 |
17 | 14, 16 | wcel 1977 |
. . . . . 6
wff (𝑦 + 𝑘) ∈ dom 𝑓 |
18 | | cc0 9815 |
. . . . . . 7
class
0 |
19 | 2 | cv 1474 |
. . . . . . 7
class 𝑛 |
20 | | cfz 12197 |
. . . . . . 7
class
... |
21 | 18, 19, 20 | co 6549 |
. . . . . 6
class
(0...𝑛) |
22 | 17, 11, 21 | wral 2896 |
. . . . 5
wff
∀𝑘 ∈
(0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓 |
23 | 22, 9, 5 | crab 2900 |
. . . 4
class {𝑦 ∈ ℂ ∣
∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} |
24 | | cbc 12951 |
. . . . . . 7
class
C |
25 | 19, 12, 24 | co 6549 |
. . . . . 6
class (𝑛C𝑘) |
26 | | c1 9816 |
. . . . . . . . 9
class
1 |
27 | 26 | cneg 10146 |
. . . . . . . 8
class
-1 |
28 | | cmin 10145 |
. . . . . . . . 9
class
− |
29 | 19, 12, 28 | co 6549 |
. . . . . . . 8
class (𝑛 − 𝑘) |
30 | | cexp 12722 |
. . . . . . . 8
class
↑ |
31 | 27, 29, 30 | co 6549 |
. . . . . . 7
class
(-1↑(𝑛 −
𝑘)) |
32 | 8 | cv 1474 |
. . . . . . . . 9
class 𝑥 |
33 | 32, 12, 13 | co 6549 |
. . . . . . . 8
class (𝑥 + 𝑘) |
34 | 33, 15 | cfv 5804 |
. . . . . . 7
class (𝑓‘(𝑥 + 𝑘)) |
35 | | cmul 9820 |
. . . . . . 7
class
· |
36 | 31, 34, 35 | co 6549 |
. . . . . 6
class
((-1↑(𝑛 −
𝑘)) · (𝑓‘(𝑥 + 𝑘))) |
37 | 25, 36, 35 | co 6549 |
. . . . 5
class ((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))) |
38 | 21, 37, 11 | csu 14264 |
. . . 4
class
Σ𝑘 ∈
(0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))) |
39 | 8, 23, 38 | cmpt 4643 |
. . 3
class (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))) |
40 | 2, 3, 4, 7, 39 | cmpt2 6551 |
. 2
class (𝑛 ∈ ℕ0,
𝑓 ∈ (ℂ
↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))))) |
41 | 1, 40 | wceq 1475 |
1
wff
△n = (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ
↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))))) |