Metamath Proof Explorer


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 syl5eq
 |-  ( 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 ) ) ) ) ) )