Detailed syntax breakdown of Definition df-tayl
Step | Hyp | Ref
| Expression |
1 | | ctayl 25245 |
. 2
class
Tayl |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | cr 10728 |
. . . 4
class
ℝ |
5 | | cc 10727 |
. . . 4
class
ℂ |
6 | 4, 5 | cpr 4543 |
. . 3
class {ℝ,
ℂ} |
7 | 2 | cv 1542 |
. . . 4
class 𝑠 |
8 | | cpm 8509 |
. . . 4
class
↑pm |
9 | 5, 7, 8 | co 7213 |
. . 3
class (ℂ
↑pm 𝑠) |
10 | | vn |
. . . 4
setvar 𝑛 |
11 | | va |
. . . 4
setvar 𝑎 |
12 | | cn0 12090 |
. . . . 5
class
ℕ0 |
13 | | cpnf 10864 |
. . . . . 6
class
+∞ |
14 | 13 | csn 4541 |
. . . . 5
class
{+∞} |
15 | 12, 14 | cun 3864 |
. . . 4
class
(ℕ0 ∪ {+∞}) |
16 | | vk |
. . . . 5
setvar 𝑘 |
17 | | cc0 10729 |
. . . . . . 7
class
0 |
18 | 10 | cv 1542 |
. . . . . . 7
class 𝑛 |
19 | | cicc 12938 |
. . . . . . 7
class
[,] |
20 | 17, 18, 19 | co 7213 |
. . . . . 6
class
(0[,]𝑛) |
21 | | cz 12176 |
. . . . . 6
class
ℤ |
22 | 20, 21 | cin 3865 |
. . . . 5
class
((0[,]𝑛) ∩
ℤ) |
23 | 16 | cv 1542 |
. . . . . . 7
class 𝑘 |
24 | 3 | cv 1542 |
. . . . . . . 8
class 𝑓 |
25 | | cdvn 24761 |
. . . . . . . 8
class
D𝑛 |
26 | 7, 24, 25 | co 7213 |
. . . . . . 7
class (𝑠 D𝑛 𝑓) |
27 | 23, 26 | cfv 6380 |
. . . . . 6
class ((𝑠 D𝑛 𝑓)‘𝑘) |
28 | 27 | cdm 5551 |
. . . . 5
class dom
((𝑠 D𝑛
𝑓)‘𝑘) |
29 | 16, 22, 28 | ciin 4905 |
. . . 4
class ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) |
30 | | vx |
. . . . 5
setvar 𝑥 |
31 | 30 | cv 1542 |
. . . . . . 7
class 𝑥 |
32 | 31 | csn 4541 |
. . . . . 6
class {𝑥} |
33 | | ccnfld 20363 |
. . . . . . 7
class
ℂfld |
34 | 11 | cv 1542 |
. . . . . . . . . . 11
class 𝑎 |
35 | 34, 27 | cfv 6380 |
. . . . . . . . . 10
class (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) |
36 | | cfa 13839 |
. . . . . . . . . . 11
class
! |
37 | 23, 36 | cfv 6380 |
. . . . . . . . . 10
class
(!‘𝑘) |
38 | | cdiv 11489 |
. . . . . . . . . 10
class
/ |
39 | 35, 37, 38 | co 7213 |
. . . . . . . . 9
class ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) |
40 | | cmin 11062 |
. . . . . . . . . . 11
class
− |
41 | 31, 34, 40 | co 7213 |
. . . . . . . . . 10
class (𝑥 − 𝑎) |
42 | | cexp 13635 |
. . . . . . . . . 10
class
↑ |
43 | 41, 23, 42 | co 7213 |
. . . . . . . . 9
class ((𝑥 − 𝑎)↑𝑘) |
44 | | cmul 10734 |
. . . . . . . . 9
class
· |
45 | 39, 43, 44 | co 7213 |
. . . . . . . 8
class
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)) |
46 | 16, 22, 45 | cmpt 5135 |
. . . . . . 7
class (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) |
47 | | ctsu 23023 |
. . . . . . 7
class
tsums |
48 | 33, 46, 47 | co 7213 |
. . . . . 6
class
(ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) |
49 | 32, 48 | cxp 5549 |
. . . . 5
class ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) |
50 | 30, 5, 49 | ciun 4904 |
. . . 4
class ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) |
51 | 10, 11, 15, 29, 50 | cmpo 7215 |
. . 3
class (𝑛 ∈ (ℕ0
∪ {+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
52 | 2, 3, 6, 9, 51 | cmpo 7215 |
. 2
class (𝑠 ∈ {ℝ, ℂ},
𝑓 ∈ (ℂ
↑pm 𝑠)
↦ (𝑛 ∈
(ℕ0 ∪ {+∞}), 𝑎 ∈ ∩
𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
53 | 1, 52 | wceq 1543 |
1
wff Tayl =
(𝑠 ∈ {ℝ,
ℂ}, 𝑓 ∈ (ℂ
↑pm 𝑠)
↦ (𝑛 ∈
(ℕ0 ∪ {+∞}), 𝑎 ∈ ∩
𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |