Definition df-tayl 23913

Description: Define the Taylor polynomial or Taylor series of a function. TODO-AV: 𝑛 ∈ (ℕ₀ ∪ {+∞}) can/should be replaced by 𝑛 ∈ ℕ₀^*. (Contributed by Mario Carneiro, 30-Dec-2016.)

Assertion

Ref	Expression
df-tayl	⊢ Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))))

Distinct variable group:   𝑘,𝑎,𝑛,𝑥,𝑓,𝑠

Detailed syntax breakdown of Definition df-tayl

Step	Hyp	Ref	Expression
1		ctayl 23911	. 2 class Tayl
2		vs	. . 3 setvar 𝑠
3		vf	. . 3 setvar 𝑓
4		cr 9814	. . . 4 class ℝ
5		cc 9813	. . . 4 class ℂ
6	4, 5	cpr 4127	. . 3 class {ℝ, ℂ}
7	2	cv 1474	. . . 4 class 𝑠
8		cpm 7745	. . . 4 class ↑pm
9	5, 7, 8	co 6549	. . 3 class (ℂ ↑pm 𝑠)
10		vn	. . . 4 setvar 𝑛
11		va	. . . 4 setvar 𝑎
12		cn0 11169	. . . . 5 class ℕ0
13		cpnf 9950	. . . . . 6 class +∞
14	13	csn 4125	. . . . 5 class {+∞}
15	12, 14	cun 3538	. . . 4 class (ℕ0 ∪ {+∞})
16		vk	. . . . 5 setvar 𝑘
17		cc0 9815	. . . . . . 7 class 0
18	10	cv 1474	. . . . . . 7 class 𝑛
19		cicc 12049	. . . . . . 7 class [,]
20	17, 18, 19	co 6549	. . . . . 6 class (0[,]𝑛)
21		cz 11254	. . . . . 6 class ℤ
22	20, 21	cin 3539	. . . . 5 class ((0[,]𝑛) ∩ ℤ)
23	16	cv 1474	. . . . . . 7 class 𝑘
24	3	cv 1474	. . . . . . . 8 class 𝑓
25		cdvn 23434	. . . . . . . 8 class D𝑛
26	7, 24, 25	co 6549	. . . . . . 7 class (𝑠 D𝑛 𝑓)
27	23, 26	cfv 5804	. . . . . 6 class ((𝑠 D𝑛 𝑓)‘𝑘)
28	27	cdm 5038	. . . . 5 class dom ((𝑠 D𝑛 𝑓)‘𝑘)
29	16, 22, 28	ciin 4456	. . . 4 class ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘)
30		vx	. . . . 5 setvar 𝑥
31	30	cv 1474	. . . . . . 7 class 𝑥
32	31	csn 4125	. . . . . 6 class {𝑥}
33		ccnfld 19567	. . . . . . 7 class ℂfld
34	11	cv 1474	. . . . . . . . . . 11 class 𝑎
35	34, 27	cfv 5804	. . . . . . . . . 10 class (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎)
36		cfa 12922	. . . . . . . . . . 11 class !
37	23, 36	cfv 5804	. . . . . . . . . 10 class (!‘𝑘)
38		cdiv 10563	. . . . . . . . . 10 class /
39	35, 37, 38	co 6549	. . . . . . . . 9 class ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘))
40		cmin 10145	. . . . . . . . . . 11 class −
41	31, 34, 40	co 6549	. . . . . . . . . 10 class (𝑥 − 𝑎)
42		cexp 12722	. . . . . . . . . 10 class ↑
43	41, 23, 42	co 6549	. . . . . . . . 9 class ((𝑥 − 𝑎)↑𝑘)
44		cmul 9820	. . . . . . . . 9 class ·
45	39, 43, 44	co 6549	. . . . . . . 8 class (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))
46	16, 22, 45	cmpt 4643	. . . . . . 7 class (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))
47		ctsu 21739	. . . . . . 7 class tsums
48	33, 46, 47	co 6549	. . . . . 6 class (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))
49	32, 48	cxp 5036	. . . . 5 class ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))
50	30, 5, 49	ciun 4455	. . . 4 class ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))
51	10, 11, 15, 29, 50	cmpt2 6551	. . 3 class (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))
52	2, 3, 6, 9, 51	cmpt2 6551	. 2 class (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))))
53	1, 52	wceq 1475	1 wff Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))))

This definition is referenced by:  taylfval  23917