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	|- ( ph -> S e. { RR , CC } )
	taylpfval.f	|- ( ph -> F : A --> CC )
	taylpfval.a	|- ( ph -> A C_ S )
	taylpfval.n	|- ( ph -> N e. NN0 )
	taylpfval.b	|- ( ph -> B e. dom ( ( S Dn F ) ` N ) )
	taylpfval.t	|- T = ( N ( S Tayl F ) B )
Assertion	taylpf	|- ( ph -> T : CC --> CC )

Proof

Step	Hyp	Ref	Expression
1		taylpfval.s	|- ( ph -> S e. { RR , CC } )
2		taylpfval.f	|- ( ph -> F : A --> CC )
3		taylpfval.a	|- ( ph -> A C_ S )
4		taylpfval.n	|- ( ph -> N e. NN0 )
5		taylpfval.b	|- ( ph -> B e. dom ( ( S Dn F ) ` N ) )
6		taylpfval.t	|- T = ( N ( S Tayl F ) B )
7	1 2 3 4 5 6	taylpfval	|- ( ph -> T = ( x e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) )
8		fzfid	|- ( ( ph /\ x e. CC ) -> ( 0 ... N ) e. Fin )
9	1 2 3 4 5	taylplem2	|- ( ( ( ph /\ x e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) e. CC )
10	8 9	fsumcl	|- ( ( ph /\ x e. CC ) -> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) e. CC )
11	7 10	fmpt3d	|- ( ph -> T : CC --> CC )