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