# Metamath Proof Explorer

## Definition df-tayl

Description: Define the Taylor polynomial or Taylor series of a function. TODO-AV: n e. ( NN0 u. { +oo } ) should be replaced by n e. NN0* . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Assertion df-tayl ${⊢}\mathrm{Tayl}=\left({s}\in \left\{ℝ,ℂ\right\},{f}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)⟼\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)⟼\bigcup _{{x}\in ℂ}\left(\left\{{x}\right\}×\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{n}\right]\cap ℤ\right)⟼\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ctayl ${class}\mathrm{Tayl}$
1 vs ${setvar}{s}$
2 cr ${class}ℝ$
3 cc ${class}ℂ$
4 2 3 cpr ${class}\left\{ℝ,ℂ\right\}$
5 vf ${setvar}{f}$
6 cpm ${class}{↑}_{𝑝𝑚}$
7 1 cv ${setvar}{s}$
8 3 7 6 co ${class}\left(ℂ{↑}_{𝑝𝑚}{s}\right)$
9 vn ${setvar}{n}$
10 cn0 ${class}{ℕ}_{0}$
11 cpnf ${class}\mathrm{+\infty }$
12 11 csn ${class}\left\{\mathrm{+\infty }\right\}$
13 10 12 cun ${class}\left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right)$
14 va ${setvar}{a}$
15 vk ${setvar}{k}$
16 cc0 ${class}0$
17 cicc ${class}\left[.\right]$
18 9 cv ${setvar}{n}$
19 16 18 17 co ${class}\left[0,{n}\right]$
20 cz ${class}ℤ$
21 19 20 cin ${class}\left(\left[0,{n}\right]\cap ℤ\right)$
22 cdvn ${class}{D}^{n}$
23 5 cv ${setvar}{f}$
24 7 23 22 co ${class}\left({s}{D}^{n}{f}\right)$
25 15 cv ${setvar}{k}$
26 25 24 cfv ${class}\left({s}{D}^{n}{f}\right)\left({k}\right)$
27 26 cdm ${class}\mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)$
28 15 21 27 ciin ${class}\bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)$
29 vx ${setvar}{x}$
30 29 cv ${setvar}{x}$
31 30 csn ${class}\left\{{x}\right\}$
32 ccnfld ${class}{ℂ}_{\mathrm{fld}}$
33 ctsu ${class}\mathrm{tsums}$
34 14 cv ${setvar}{a}$
35 34 26 cfv ${class}\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)$
36 cdiv ${class}÷$
37 cfa ${class}!$
38 25 37 cfv ${class}{k}!$
39 35 38 36 co ${class}\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right)$
40 cmul ${class}×$
41 cmin ${class}-$
42 30 34 41 co ${class}\left({x}-{a}\right)$
43 cexp ${class}^$
44 42 25 43 co ${class}{\left({x}-{a}\right)}^{{k}}$
45 39 44 40 co ${class}\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}$
46 15 21 45 cmpt ${class}\left({k}\in \left(\left[0,{n}\right]\cap ℤ\right)⟼\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)$
47 32 46 33 co ${class}\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{n}\right]\cap ℤ\right)⟼\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)$
48 31 47 cxp ${class}\left(\left\{{x}\right\}×\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{n}\right]\cap ℤ\right)⟼\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)$
49 29 3 48 ciun ${class}\bigcup _{{x}\in ℂ}\left(\left\{{x}\right\}×\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{n}\right]\cap ℤ\right)⟼\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)$
50 9 14 13 28 49 cmpo ${class}\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)⟼\bigcup _{{x}\in ℂ}\left(\left\{{x}\right\}×\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{n}\right]\cap ℤ\right)⟼\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)$
51 1 5 4 8 50 cmpo ${class}\left({s}\in \left\{ℝ,ℂ\right\},{f}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)⟼\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)⟼\bigcup _{{x}\in ℂ}\left(\left\{{x}\right\}×\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{n}\right]\cap ℤ\right)⟼\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)\right)$
52 0 51 wceq ${wff}\mathrm{Tayl}=\left({s}\in \left\{ℝ,ℂ\right\},{f}\in \left(ℂ{↑}_{𝑝𝑚}{s}\right)⟼\left({n}\in \left({ℕ}_{0}\cup \left\{\mathrm{+\infty }\right\}\right),{a}\in \bigcap _{{k}\in \left[0,{n}\right]\cap ℤ}\mathrm{dom}\left({s}{D}^{n}{f}\right)\left({k}\right)⟼\bigcup _{{x}\in ℂ}\left(\left\{{x}\right\}×\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left({k}\in \left(\left[0,{n}\right]\cap ℤ\right)⟼\left(\frac{\left({s}{D}^{n}{f}\right)\left({k}\right)\left({a}\right)}{{k}!}\right){\left({x}-{a}\right)}^{{k}}\right)\right)\right)\right)\right)$