Detailed syntax breakdown of Definition df-tayl
Step | Hyp | Ref
| Expression |
1 | | ctayl 24107 |
. 2
class
Tayl |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | cr 9935 |
. . . 4
class
ℝ |
5 | | cc 9934 |
. . . 4
class
ℂ |
6 | 4, 5 | cpr 4179 |
. . 3
class {ℝ,
ℂ} |
7 | 2 | cv 1482 |
. . . 4
class 𝑠 |
8 | | cpm 7858 |
. . . 4
class
↑pm |
9 | 5, 7, 8 | co 6650 |
. . 3
class (ℂ
↑pm 𝑠) |
10 | | vn |
. . . 4
setvar 𝑛 |
11 | | va |
. . . 4
setvar 𝑎 |
12 | | cn0 11292 |
. . . . 5
class
ℕ0 |
13 | | cpnf 10071 |
. . . . . 6
class
+∞ |
14 | 13 | csn 4177 |
. . . . 5
class
{+∞} |
15 | 12, 14 | cun 3572 |
. . . 4
class
(ℕ0 ∪ {+∞}) |
16 | | vk |
. . . . 5
setvar 𝑘 |
17 | | cc0 9936 |
. . . . . . 7
class
0 |
18 | 10 | cv 1482 |
. . . . . . 7
class 𝑛 |
19 | | cicc 12178 |
. . . . . . 7
class
[,] |
20 | 17, 18, 19 | co 6650 |
. . . . . 6
class
(0[,]𝑛) |
21 | | cz 11377 |
. . . . . 6
class
ℤ |
22 | 20, 21 | cin 3573 |
. . . . 5
class
((0[,]𝑛) ∩
ℤ) |
23 | 16 | cv 1482 |
. . . . . . 7
class 𝑘 |
24 | 3 | cv 1482 |
. . . . . . . 8
class 𝑓 |
25 | | cdvn 23628 |
. . . . . . . 8
class
D𝑛 |
26 | 7, 24, 25 | co 6650 |
. . . . . . 7
class (𝑠 D𝑛 𝑓) |
27 | 23, 26 | cfv 5888 |
. . . . . 6
class ((𝑠 D𝑛 𝑓)‘𝑘) |
28 | 27 | cdm 5114 |
. . . . 5
class dom
((𝑠 D𝑛
𝑓)‘𝑘) |
29 | 16, 22, 28 | ciin 4521 |
. . . 4
class ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) |
30 | | vx |
. . . . 5
setvar 𝑥 |
31 | 30 | cv 1482 |
. . . . . . 7
class 𝑥 |
32 | 31 | csn 4177 |
. . . . . 6
class {𝑥} |
33 | | ccnfld 19746 |
. . . . . . 7
class
ℂfld |
34 | 11 | cv 1482 |
. . . . . . . . . . 11
class 𝑎 |
35 | 34, 27 | cfv 5888 |
. . . . . . . . . 10
class (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) |
36 | | cfa 13060 |
. . . . . . . . . . 11
class
! |
37 | 23, 36 | cfv 5888 |
. . . . . . . . . 10
class
(!‘𝑘) |
38 | | cdiv 10684 |
. . . . . . . . . 10
class
/ |
39 | 35, 37, 38 | co 6650 |
. . . . . . . . 9
class ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) |
40 | | cmin 10266 |
. . . . . . . . . . 11
class
− |
41 | 31, 34, 40 | co 6650 |
. . . . . . . . . 10
class (𝑥 − 𝑎) |
42 | | cexp 12860 |
. . . . . . . . . 10
class
↑ |
43 | 41, 23, 42 | co 6650 |
. . . . . . . . 9
class ((𝑥 − 𝑎)↑𝑘) |
44 | | cmul 9941 |
. . . . . . . . 9
class
· |
45 | 39, 43, 44 | co 6650 |
. . . . . . . 8
class
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)) |
46 | 16, 22, 45 | cmpt 4729 |
. . . . . . 7
class (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) |
47 | | ctsu 21929 |
. . . . . . 7
class
tsums |
48 | 33, 46, 47 | co 6650 |
. . . . . 6
class
(ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) |
49 | 32, 48 | cxp 5112 |
. . . . 5
class ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) |
50 | 30, 5, 49 | ciun 4520 |
. . . 4
class ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) |
51 | 10, 11, 15, 29, 50 | cmpt2 6652 |
. . 3
class (𝑛 ∈ (ℕ0
∪ {+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
52 | 2, 3, 6, 9, 51 | cmpt2 6652 |
. 2
class (𝑠 ∈ {ℝ, ℂ},
𝑓 ∈ (ℂ
↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
53 | 1, 52 | wceq 1483 |
1
wff Tayl =
(𝑠 ∈ {ℝ,
ℂ}, 𝑓 ∈ (ℂ
↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |