Theorem taylpf

Description: The Taylor polynomial is a function on the complex numbers (even if the base set of the original function is the reals). (Contributed by Mario Carneiro, 31-Dec-2016)

	Ref	Expression
Hypotheses	taylpfval.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	taylpfval.f	$$⊢\phi \to F:A⟶ℂ$$
	taylpfval.a	$$⊢\phi \to A\subseteq S$$
	taylpfval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	taylpfval.b	$$⊢\phi \to B\in \mathrm{dom}\left(S{D}^{n}F\right)\left(N\right)$$
	taylpfval.t	$$⊢T=N\left(S\mathrm{Tayl}F\right)B$$
Assertion	taylpf	$$⊢\phi \to T:ℂ⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		taylpfval.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		taylpfval.f	$$⊢\phi \to F:A⟶ℂ$$
3		taylpfval.a	$$⊢\phi \to A\subseteq S$$
4		taylpfval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		taylpfval.b	$$⊢\phi \to B\in \mathrm{dom}\left(S{D}^{n}F\right)\left(N\right)$$
6		taylpfval.t	$$⊢T=N\left(S\mathrm{Tayl}F\right)B$$
7	1 2 3 4 5 6	taylpfval	$$⊢\phi \to T=\left(x\in ℂ⟼\sum _{k=0}^N\left(\frac{\left(S{D}^{n}F\right)\left(k\right)\left(B\right)}{k!}\right){\left(x-B\right)}^k\right)$$
8		fzfid	$$⊢\left(\phi \wedge x\in ℂ\right)\to \left(0\dots N\right)\in \mathrm{Fin}$$
9	1 2 3 4 5	taylplem2	$$⊢\left(\left(\phi \wedge x\in ℂ\right)\wedge k\in \left(0\dots N\right)\right)\to \left(\frac{\left(S{D}^{n}F\right)\left(k\right)\left(B\right)}{k!}\right){\left(x-B\right)}^k\in ℂ$$
10	8 9	fsumcl	$$⊢\left(\phi \wedge x\in ℂ\right)\to \sum _{k=0}^N\left(\frac{\left(S{D}^{n}F\right)\left(k\right)\left(B\right)}{k!}\right){\left(x-B\right)}^k\in ℂ$$
11	7 10	fmpt3d	$$⊢\phi \to T:ℂ⟶ℂ$$