Definition df-tayl 25867

Description: Define the Taylor polynomial or Taylor series of a function. TODO-AV: 𝑛 ∈ (ℕ₀ ∪ {+∞}) 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 25865	. 2 class Tayl
2		vs	. . 3 setvar 𝑠
3		vf	. . 3 setvar 𝑓
4		cr 11109	. . . 4 class ℝ
5		cc 11108	. . . 4 class ℂ
6	4, 5	cpr 4631	. . 3 class {ℝ, ℂ}
7	2	cv 1541	. . . 4 class 𝑠
8		cpm 8821	. . . 4 class ↑pm
9	5, 7, 8	co 7409	. . 3 class (ℂ ↑pm 𝑠)
10		vn	. . . 4 setvar 𝑛
11		va	. . . 4 setvar 𝑎
12		cn0 12472	. . . . 5 class ℕ0
13		cpnf 11245	. . . . . 6 class +∞
14	13	csn 4629	. . . . 5 class {+∞}
15	12, 14	cun 3947	. . . 4 class (ℕ0 ∪ {+∞})
16		vk	. . . . 5 setvar 𝑘
17		cc0 11110	. . . . . . 7 class 0
18	10	cv 1541	. . . . . . 7 class 𝑛
19		cicc 13327	. . . . . . 7 class [,]
20	17, 18, 19	co 7409	. . . . . 6 class (0[,]𝑛)
21		cz 12558	. . . . . 6 class ℤ
22	20, 21	cin 3948	. . . . 5 class ((0[,]𝑛) ∩ ℤ)
23	16	cv 1541	. . . . . . 7 class 𝑘
24	3	cv 1541	. . . . . . . 8 class 𝑓
25		cdvn 25381	. . . . . . . 8 class D𝑛
26	7, 24, 25	co 7409	. . . . . . 7 class (𝑠 D𝑛 𝑓)
27	23, 26	cfv 6544	. . . . . 6 class ((𝑠 D𝑛 𝑓)‘𝑘)
28	27	cdm 5677	. . . . 5 class dom ((𝑠 D𝑛 𝑓)‘𝑘)
29	16, 22, 28	ciin 4999	. . . 4 class ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘)
30		vx	. . . . 5 setvar 𝑥
31	30	cv 1541	. . . . . . 7 class 𝑥
32	31	csn 4629	. . . . . 6 class {𝑥}
33		ccnfld 20944	. . . . . . 7 class ℂfld
34	11	cv 1541	. . . . . . . . . . 11 class 𝑎
35	34, 27	cfv 6544	. . . . . . . . . 10 class (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎)
36		cfa 14233	. . . . . . . . . . 11 class !
37	23, 36	cfv 6544	. . . . . . . . . 10 class (!‘𝑘)
38		cdiv 11871	. . . . . . . . . 10 class /
39	35, 37, 38	co 7409	. . . . . . . . 9 class ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘))
40		cmin 11444	. . . . . . . . . . 11 class −
41	31, 34, 40	co 7409	. . . . . . . . . 10 class (𝑥 − 𝑎)
42		cexp 14027	. . . . . . . . . 10 class ↑
43	41, 23, 42	co 7409	. . . . . . . . 9 class ((𝑥 − 𝑎)↑𝑘)
44		cmul 11115	. . . . . . . . 9 class ·
45	39, 43, 44	co 7409	. . . . . . . 8 class (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))
46	16, 22, 45	cmpt 5232	. . . . . . 7 class (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))
47		ctsu 23630	. . . . . . 7 class tsums
48	33, 46, 47	co 7409	. . . . . 6 class (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))
49	32, 48	cxp 5675	. . . . 5 class ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))
50	30, 5, 49	ciun 4998	. . . 4 class ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))
51	10, 11, 15, 29, 50	cmpo 7411	. . 3 class (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))
52	2, 3, 6, 9, 51	cmpo 7411	. 2 class (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))))
53	1, 52	wceq 1542	1 wff Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))))

This definition is referenced by:  taylfval  25871