Theorem taylfval

Description: Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: S is the base set with respect to evaluate the derivatives (generally RR or CC ), F is the function we are approximating, at point B , to order N . The result is a polynomial function of x .

This "extended" version of taylpfval additionally handles the case N = +oo , in which case this is not a polynomial but an infinite series, the Taylor series of the function. (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Hypotheses	taylfval.s	|- ( ph -> S e. { RR , CC } )
	taylfval.f	|- ( ph -> F : A --> CC )
	taylfval.a	|- ( ph -> A C_ S )
	taylfval.n	|- ( ph -> ( N e. NN0 \/ N = +oo ) )
	taylfval.b	|- ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )
	taylfval.t	|- T = ( N ( S Tayl F ) B )
Assertion	taylfval	|- ( ph -> T = U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		taylfval.s	|- ( ph -> S e. { RR , CC } )
2		taylfval.f	|- ( ph -> F : A --> CC )
3		taylfval.a	|- ( ph -> A C_ S )
4		taylfval.n	|- ( ph -> ( N e. NN0 \/ N = +oo ) )
5		taylfval.b	|- ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )
6		taylfval.t	|- T = ( N ( S Tayl F ) B )
7		df-tayl	|- Tayl = ( s e. { RR , CC } , f e. ( CC ^pm s ) |-> ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( s Dn f ) ` k ) |-> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) )
8	7	a1i	|- ( ph -> Tayl = ( s e. { RR , CC } , f e. ( CC ^pm s ) |-> ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( s Dn f ) ` k ) |-> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) ) )
9		eqidd	|- ( ( ph /\ ( s = S /\ f = F ) ) -> ( NN0 u. { +oo } ) = ( NN0 u. { +oo } ) )
10		oveq12	|- ( ( s = S /\ f = F ) -> ( s Dn f ) = ( S Dn F ) )
11	10	ad2antlr	|- ( ( ( ph /\ ( s = S /\ f = F ) ) /\ k e. ( ( 0 [,] n ) i^i ZZ ) ) -> ( s Dn f ) = ( S Dn F ) )
12	11	fveq1d	|- ( ( ( ph /\ ( s = S /\ f = F ) ) /\ k e. ( ( 0 [,] n ) i^i ZZ ) ) -> ( ( s Dn f ) ` k ) = ( ( S Dn F ) ` k ) )
13	12	dmeqd	|- ( ( ( ph /\ ( s = S /\ f = F ) ) /\ k e. ( ( 0 [,] n ) i^i ZZ ) ) -> dom ( ( s Dn f ) ` k ) = dom ( ( S Dn F ) ` k ) )
14	13	iineq2dv	|- ( ( ph /\ ( s = S /\ f = F ) ) -> |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( s Dn f ) ` k ) = |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) )
15	12	fveq1d	|- ( ( ( ph /\ ( s = S /\ f = F ) ) /\ k e. ( ( 0 [,] n ) i^i ZZ ) ) -> ( ( ( s Dn f ) ` k ) ` a ) = ( ( ( S Dn F ) ` k ) ` a ) )
16	15	oveq1d	|- ( ( ( ph /\ ( s = S /\ f = F ) ) /\ k e. ( ( 0 [,] n ) i^i ZZ ) ) -> ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) = ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) )
17	16	oveq1d	|- ( ( ( ph /\ ( s = S /\ f = F ) ) /\ k e. ( ( 0 [,] n ) i^i ZZ ) ) -> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) = ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) )
18	17	mpteq2dva	|- ( ( ph /\ ( s = S /\ f = F ) ) -> ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) = ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) )
19	18	oveq2d	|- ( ( ph /\ ( s = S /\ f = F ) ) -> ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) = ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) )
20	19	xpeq2d	|- ( ( ph /\ ( s = S /\ f = F ) ) -> ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) = ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) )
21	20	iuneq2d	|- ( ( ph /\ ( s = S /\ f = F ) ) -> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) = U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) )
22	9 14 21	mpoeq123dv	|- ( ( ph /\ ( s = S /\ f = F ) ) -> ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( s Dn f ) ` k ) |-> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) = ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) |-> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) )
23		simpr	|- ( ( ph /\ s = S ) -> s = S )
24	23	oveq2d	|- ( ( ph /\ s = S ) -> ( CC ^pm s ) = ( CC ^pm S ) )
25		cnex	|- CC e. _V
26	25	a1i	|- ( ph -> CC e. _V )
27		elpm2r	|- ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
28	26 1 2 3 27	syl22anc	|- ( ph -> F e. ( CC ^pm S ) )
29		nn0ex	|- NN0 e. _V
30		snex	|- { +oo } e. _V
31	29 30	unex	|- ( NN0 u. { +oo } ) e. _V
32		0xr	|- 0 e. RR*
33		nn0ssre	|- NN0 C_ RR
34		ressxr	|- RR C_ RR*
35	33 34	sstri	|- NN0 C_ RR*
36		pnfxr	|- +oo e. RR*
37		snssi	|- ( +oo e. RR* -> { +oo } C_ RR* )
38	36 37	ax-mp	|- { +oo } C_ RR*
39	35 38	unssi	|- ( NN0 u. { +oo } ) C_ RR*
40	39	sseli	|- ( n e. ( NN0 u. { +oo } ) -> n e. RR* )
41		elun	|- ( n e. ( NN0 u. { +oo } ) <-> ( n e. NN0 \/ n e. { +oo } ) )
42		nn0ge0	|- ( n e. NN0 -> 0 <_ n )
43		0lepnf	|- 0 <_ +oo
44		elsni	|- ( n e. { +oo } -> n = +oo )
45	43 44	breqtrrid	|- ( n e. { +oo } -> 0 <_ n )
46	42 45	jaoi	|- ( ( n e. NN0 \/ n e. { +oo } ) -> 0 <_ n )
47	41 46	sylbi	|- ( n e. ( NN0 u. { +oo } ) -> 0 <_ n )
48		lbicc2	|- ( ( 0 e. RR* /\ n e. RR* /\ 0 <_ n ) -> 0 e. ( 0 [,] n ) )
49	32 40 47 48	mp3an2i	|- ( n e. ( NN0 u. { +oo } ) -> 0 e. ( 0 [,] n ) )
50		0z	|- 0 e. ZZ
51		inelcm	|- ( ( 0 e. ( 0 [,] n ) /\ 0 e. ZZ ) -> ( ( 0 [,] n ) i^i ZZ ) =/= (/) )
52	49 50 51	sylancl	|- ( n e. ( NN0 u. { +oo } ) -> ( ( 0 [,] n ) i^i ZZ ) =/= (/) )
53		fvex	|- ( ( S Dn F ) ` k ) e. _V
54	53	dmex	|- dom ( ( S Dn F ) ` k ) e. _V
55	54	rgenw	|- A. k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) e. _V
56		iinexg	|- ( ( ( ( 0 [,] n ) i^i ZZ ) =/= (/) /\ A. k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) e. _V ) -> |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) e. _V )
57	52 55 56	sylancl	|- ( n e. ( NN0 u. { +oo } ) -> |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) e. _V )
58	57	rgen	|- A. n e. ( NN0 u. { +oo } ) |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) e. _V
59		eqid	|- ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) |-> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) = ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) |-> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) )
60	59	mpoexxg	|- ( ( ( NN0 u. { +oo } ) e. _V /\ A. n e. ( NN0 u. { +oo } ) |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) e. _V ) -> ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) |-> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) e. _V )
61	31 58 60	mp2an	|- ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) |-> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) e. _V
62	61	a1i	|- ( ph -> ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) |-> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) e. _V )
63	8 22 24 1 28 62	ovmpodx	|- ( ph -> ( S Tayl F ) = ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) |-> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) )
64		simprl	|- ( ( ph /\ ( n = N /\ a = B ) ) -> n = N )
65	64	oveq2d	|- ( ( ph /\ ( n = N /\ a = B ) ) -> ( 0 [,] n ) = ( 0 [,] N ) )
66	65	ineq1d	|- ( ( ph /\ ( n = N /\ a = B ) ) -> ( ( 0 [,] n ) i^i ZZ ) = ( ( 0 [,] N ) i^i ZZ ) )
67		simprr	|- ( ( ph /\ ( n = N /\ a = B ) ) -> a = B )
68	67	fveq2d	|- ( ( ph /\ ( n = N /\ a = B ) ) -> ( ( ( S Dn F ) ` k ) ` a ) = ( ( ( S Dn F ) ` k ) ` B ) )
69	68	oveq1d	|- ( ( ph /\ ( n = N /\ a = B ) ) -> ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) = ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) )
70	67	oveq2d	|- ( ( ph /\ ( n = N /\ a = B ) ) -> ( x - a ) = ( x - B ) )
71	70	oveq1d	|- ( ( ph /\ ( n = N /\ a = B ) ) -> ( ( x - a ) ^ k ) = ( ( x - B ) ^ k ) )
72	69 71	oveq12d	|- ( ( ph /\ ( n = N /\ a = B ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) )
73	66 72	mpteq12dv	|- ( ( ph /\ ( n = N /\ a = B ) ) -> ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) = ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) )
74	73	oveq2d	|- ( ( ph /\ ( n = N /\ a = B ) ) -> ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) = ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) )
75	74	xpeq2d	|- ( ( ph /\ ( n = N /\ a = B ) ) -> ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) = ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) )
76	75	iuneq2d	|- ( ( ph /\ ( n = N /\ a = B ) ) -> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) = U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) )
77		simpr	|- ( ( ph /\ n = N ) -> n = N )
78	77	oveq2d	|- ( ( ph /\ n = N ) -> ( 0 [,] n ) = ( 0 [,] N ) )
79	78	ineq1d	|- ( ( ph /\ n = N ) -> ( ( 0 [,] n ) i^i ZZ ) = ( ( 0 [,] N ) i^i ZZ ) )
80		iineq1	|- ( ( ( 0 [,] n ) i^i ZZ ) = ( ( 0 [,] N ) i^i ZZ ) -> |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) = |^|_ k e. ( ( 0 [,] N ) i^i ZZ ) dom ( ( S Dn F ) ` k ) )
81	79 80	syl	|- ( ( ph /\ n = N ) -> |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( S Dn F ) ` k ) = |^|_ k e. ( ( 0 [,] N ) i^i ZZ ) dom ( ( S Dn F ) ` k ) )
82		pnfex	|- +oo e. _V
83	82	elsn2	|- ( N e. { +oo } <-> N = +oo )
84	83	orbi2i	|- ( ( N e. NN0 \/ N e. { +oo } ) <-> ( N e. NN0 \/ N = +oo ) )
85	4 84	sylibr	|- ( ph -> ( N e. NN0 \/ N e. { +oo } ) )
86		elun	|- ( N e. ( NN0 u. { +oo } ) <-> ( N e. NN0 \/ N e. { +oo } ) )
87	85 86	sylibr	|- ( ph -> N e. ( NN0 u. { +oo } ) )
88	5	ralrimiva	|- ( ph -> A. k e. ( ( 0 [,] N ) i^i ZZ ) B e. dom ( ( S Dn F ) ` k ) )
89		oveq2	|- ( n = N -> ( 0 [,] n ) = ( 0 [,] N ) )
90	89	ineq1d	|- ( n = N -> ( ( 0 [,] n ) i^i ZZ ) = ( ( 0 [,] N ) i^i ZZ ) )
91	90	neeq1d	|- ( n = N -> ( ( ( 0 [,] n ) i^i ZZ ) =/= (/) <-> ( ( 0 [,] N ) i^i ZZ ) =/= (/) ) )
92	91 52	vtoclga	|- ( N e. ( NN0 u. { +oo } ) -> ( ( 0 [,] N ) i^i ZZ ) =/= (/) )
93	87 92	syl	|- ( ph -> ( ( 0 [,] N ) i^i ZZ ) =/= (/) )
94		r19.2z	|- ( ( ( ( 0 [,] N ) i^i ZZ ) =/= (/) /\ A. k e. ( ( 0 [,] N ) i^i ZZ ) B e. dom ( ( S Dn F ) ` k ) ) -> E. k e. ( ( 0 [,] N ) i^i ZZ ) B e. dom ( ( S Dn F ) ` k ) )
95	93 88 94	syl2anc	|- ( ph -> E. k e. ( ( 0 [,] N ) i^i ZZ ) B e. dom ( ( S Dn F ) ` k ) )
96		elex	|- ( B e. dom ( ( S Dn F ) ` k ) -> B e. _V )
97	96	rexlimivw	|- ( E. k e. ( ( 0 [,] N ) i^i ZZ ) B e. dom ( ( S Dn F ) ` k ) -> B e. _V )
98		eliin	|- ( B e. _V -> ( B e. |^|_ k e. ( ( 0 [,] N ) i^i ZZ ) dom ( ( S Dn F ) ` k ) <-> A. k e. ( ( 0 [,] N ) i^i ZZ ) B e. dom ( ( S Dn F ) ` k ) ) )
99	95 97 98	3syl	|- ( ph -> ( B e. |^|_ k e. ( ( 0 [,] N ) i^i ZZ ) dom ( ( S Dn F ) ` k ) <-> A. k e. ( ( 0 [,] N ) i^i ZZ ) B e. dom ( ( S Dn F ) ` k ) ) )
100	88 99	mpbird	|- ( ph -> B e. |^|_ k e. ( ( 0 [,] N ) i^i ZZ ) dom ( ( S Dn F ) ` k ) )
101		snssi	|- ( x e. CC -> { x } C_ CC )
102	1 2 3 4 5	taylfvallem	|- ( ( ph /\ x e. CC ) -> ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) C_ CC )
103		xpss12	|- ( ( { x } C_ CC /\ ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) C_ CC ) -> ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) )
104	101 102 103	syl2an2	|- ( ( ph /\ x e. CC ) -> ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) )
105	104	ralrimiva	|- ( ph -> A. x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) )
106		iunss	|- ( U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) <-> A. x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) )
107	105 106	sylibr	|- ( ph -> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) )
108	25 25	xpex	|- ( CC X. CC ) e. _V
109	108	ssex	|- ( U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) -> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) e. _V )
110	107 109	syl	|- ( ph -> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) e. _V )
111	63 76 81 87 100 110	ovmpodx	|- ( ph -> ( N ( S Tayl F ) B ) = U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) )
112	6 111	eqtrid	|- ( ph -> T = U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) )