Metamath Proof Explorer

Theorem dvtaylp

Description: The derivative of the Taylor polynomial is the Taylor polynomial of the derivative of the function. (Contributed by Mario Carneiro, 31-Dec-2016)

Ref Expression
Hypotheses dvtaylp.s 
|- ( ph -> S e. { RR , CC } )
dvtaylp.f 
|- ( ph -> F : A --> CC )
dvtaylp.a 
|- ( ph -> A C_ S )
dvtaylp.n 
|- ( ph -> N e. NN0 )
dvtaylp.b 
|- ( ph -> B e. dom ( ( S Dn F ) ` ( N + 1 ) ) )
Assertion dvtaylp 
|- ( ph -> ( CC _D ( ( N + 1 ) ( S Tayl F ) B ) ) = ( N ( S Tayl ( S _D F ) ) B ) )

Proof

Step Hyp Ref Expression
1 dvtaylp.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvtaylp.f 
 |-  ( ph -> F : A --> CC )
3 dvtaylp.a 
 |-  ( ph -> A C_ S )
4 dvtaylp.n 
 |-  ( ph -> N e. NN0 )
5 dvtaylp.b 
 |-  ( ph -> B e. dom ( ( S Dn F ) ` ( N + 1 ) ) )
6 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
7 6 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
8 7 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
9 cnelprrecn 
 |-  CC e. { RR , CC }
10 9 a1i 
 |-  ( ph -> CC e. { RR , CC } )
11 toponmax 
 |-  ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
12 7 11 mp1i 
 |-  ( ph -> CC e. ( TopOpen ` CCfld ) )
13 fzfid 
 |-  ( ph -> ( 0 ... ( N + 1 ) ) e. Fin )
14 cnex 
 |-  CC e. _V
15 14 a1i 
 |-  ( ph -> CC e. _V )
16 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
17 15 1 2 3 16 syl22anc 
 |-  ( ph -> F e. ( CC ^pm S ) )
18 elfznn0 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> k e. NN0 )
19 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
20 1 17 18 19 syl2an3an 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
21 0z 
 |-  0 e. ZZ
22 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
23 4 22 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
24 23 nn0zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
25 fzval2 
 |-  ( ( 0 e. ZZ /\ ( N + 1 ) e. ZZ ) -> ( 0 ... ( N + 1 ) ) = ( ( 0 [,] ( N + 1 ) ) i^i ZZ ) )
26 21 24 25 sylancr 
 |-  ( ph -> ( 0 ... ( N + 1 ) ) = ( ( 0 [,] ( N + 1 ) ) i^i ZZ ) )
27 26 eleq2d 
 |-  ( ph -> ( k e. ( 0 ... ( N + 1 ) ) <-> k e. ( ( 0 [,] ( N + 1 ) ) i^i ZZ ) ) )
28 27 biimpa 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. ( ( 0 [,] ( N + 1 ) ) i^i ZZ ) )
29 1 2 3 23 5 taylplem1 
 |-  ( ( ph /\ k e. ( ( 0 [,] ( N + 1 ) ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )
30 28 29 syldan 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> B e. dom ( ( S Dn F ) ` k ) )
31 20 30 ffvelrnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( S Dn F ) ` k ) ` B ) e. CC )
32 18 adantl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. NN0 )
33 32 faccld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ! ` k ) e. NN )
34 33 nncnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ! ` k ) e. CC )
35 33 nnne0d 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ! ` k ) =/= 0 )
36 31 34 35 divcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. CC )
37 36 3adant3 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. CC )
38 simp3 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) -> x e. CC )
39 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
40 1 39 syl 
 |-  ( ph -> S C_ CC )
41 3 40 sstrd 
 |-  ( ph -> A C_ CC )
42 dvnbss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ ( N + 1 ) e. NN0 ) -> dom ( ( S Dn F ) ` ( N + 1 ) ) C_ dom F )
43 1 17 23 42 syl3anc 
 |-  ( ph -> dom ( ( S Dn F ) ` ( N + 1 ) ) C_ dom F )
44 2 43 fssdmd 
 |-  ( ph -> dom ( ( S Dn F ) ` ( N + 1 ) ) C_ A )
45 44 5 sseldd 
 |-  ( ph -> B e. A )
46 41 45 sseldd 
 |-  ( ph -> B e. CC )
47 46 3ad2ant1 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) -> B e. CC )
48 38 47 subcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) -> ( x - B ) e. CC )
49 18 3ad2ant2 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) -> k e. NN0 )
50 48 49 expcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) -> ( ( x - B ) ^ k ) e. CC )
51 37 50 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) e. CC )
52 0cnd 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) /\ k = 0 ) -> 0 e. CC )
53 49 nn0cnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) -> k e. CC )
54 53 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) /\ -. k = 0 ) -> k e. CC )
55 48 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) /\ -. k = 0 ) -> ( x - B ) e. CC )
56 49 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) /\ -. k = 0 ) -> k e. NN0 )
57 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) /\ -. k = 0 ) -> -. k = 0 )
58 57 neqned 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) /\ -. k = 0 ) -> k =/= 0 )
59 elnnne0 
 |-  ( k e. NN <-> ( k e. NN0 /\ k =/= 0 ) )
60 56 58 59 sylanbrc 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) /\ -. k = 0 ) -> k e. NN )
61 nnm1nn0 
 |-  ( k e. NN -> ( k - 1 ) e. NN0 )
62 60 61 syl 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) /\ -. k = 0 ) -> ( k - 1 ) e. NN0 )
63 55 62 expcld 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) /\ -. k = 0 ) -> ( ( x - B ) ^ ( k - 1 ) ) e. CC )
64 54 63 mulcld 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) /\ -. k = 0 ) -> ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) e. CC )
65 52 64 ifclda 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) -> if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) e. CC )
66 37 65 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) /\ x e. CC ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) e. CC )
67 9 a1i 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> CC e. { RR , CC } )
68 50 3expa 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ x e. CC ) -> ( ( x - B ) ^ k ) e. CC )
69 65 3expa 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ x e. CC ) -> if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) e. CC )
70 48 3expa 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ x e. CC ) -> ( x - B ) e. CC )
71 1cnd 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ x e. CC ) -> 1 e. CC )
72 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ y e. CC ) -> y e. CC )
73 32 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ y e. CC ) -> k e. NN0 )
74 72 73 expcld 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ y e. CC ) -> ( y ^ k ) e. CC )
75 c0ex 
 |-  0 e. _V
76 ovex 
 |-  ( k x. ( y ^ ( k - 1 ) ) ) e. _V
77 75 76 ifex 
 |-  if ( k = 0 , 0 , ( k x. ( y ^ ( k - 1 ) ) ) ) e. _V
78 77 a1i 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ y e. CC ) -> if ( k = 0 , 0 , ( k x. ( y ^ ( k - 1 ) ) ) ) e. _V )
79 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ x e. CC ) -> x e. CC )
80 67 dvmptid 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
81 46 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ x e. CC ) -> B e. CC )
82 0cnd 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ x e. CC ) -> 0 e. CC )
83 46 adantr 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> B e. CC )
84 67 83 dvmptc 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( CC _D ( x e. CC |-> B ) ) = ( x e. CC |-> 0 ) )
85 67 79 71 80 81 82 84 dvmptsub 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( CC _D ( x e. CC |-> ( x - B ) ) ) = ( x e. CC |-> ( 1 - 0 ) ) )
86 1m0e1 
 |-  ( 1 - 0 ) = 1
87 86 mpteq2i 
 |-  ( x e. CC |-> ( 1 - 0 ) ) = ( x e. CC |-> 1 )
88 85 87 eqtrdi 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( CC _D ( x e. CC |-> ( x - B ) ) ) = ( x e. CC |-> 1 ) )
89 dvexp2 
 |-  ( k e. NN0 -> ( CC _D ( y e. CC |-> ( y ^ k ) ) ) = ( y e. CC |-> if ( k = 0 , 0 , ( k x. ( y ^ ( k - 1 ) ) ) ) ) )
90 32 89 syl 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( CC _D ( y e. CC |-> ( y ^ k ) ) ) = ( y e. CC |-> if ( k = 0 , 0 , ( k x. ( y ^ ( k - 1 ) ) ) ) ) )
91 oveq1 
 |-  ( y = ( x - B ) -> ( y ^ k ) = ( ( x - B ) ^ k ) )
92 oveq1 
 |-  ( y = ( x - B ) -> ( y ^ ( k - 1 ) ) = ( ( x - B ) ^ ( k - 1 ) ) )
93 92 oveq2d 
 |-  ( y = ( x - B ) -> ( k x. ( y ^ ( k - 1 ) ) ) = ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) )
94 93 ifeq2d 
 |-  ( y = ( x - B ) -> if ( k = 0 , 0 , ( k x. ( y ^ ( k - 1 ) ) ) ) = if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) )
95 67 67 70 71 74 78 88 90 91 94 dvmptco 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( CC _D ( x e. CC |-> ( ( x - B ) ^ k ) ) ) = ( x e. CC |-> ( if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) x. 1 ) ) )
96 69 mulid1d 
 |-  ( ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) /\ x e. CC ) -> ( if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) x. 1 ) = if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) )
97 96 mpteq2dva 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( x e. CC |-> ( if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) x. 1 ) ) = ( x e. CC |-> if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) )
98 95 97 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( CC _D ( x e. CC |-> ( ( x - B ) ^ k ) ) ) = ( x e. CC |-> if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) )
99 67 68 69 98 36 dvmptcmul 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( CC _D ( x e. CC |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) = ( x e. CC |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) ) )
100 8 6 10 12 13 51 66 99 dvmptfsum 
 |-  ( ph -> ( CC _D ( x e. CC |-> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) = ( x e. CC |-> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) ) )
101 1zzd 
 |-  ( ( ph /\ x e. CC ) -> 1 e. ZZ )
102 0zd 
 |-  ( ( ph /\ x e. CC ) -> 0 e. ZZ )
103 4 nn0zd 
 |-  ( ph -> N e. ZZ )
104 103 adantr 
 |-  ( ( ph /\ x e. CC ) -> N e. ZZ )
105 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
106 1 105 syl 
 |-  ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )
107 40 2 3 dvbss 
 |-  ( ph -> dom ( S _D F ) C_ A )
108 107 3 sstrd 
 |-  ( ph -> dom ( S _D F ) C_ S )
109 1nn0 
 |-  1 e. NN0
110 109 a1i 
 |-  ( ph -> 1 e. NN0 )
111 dvnadd 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( 1 e. NN0 /\ N e. NN0 ) ) -> ( ( S Dn ( ( S Dn F ) ` 1 ) ) ` N ) = ( ( S Dn F ) ` ( 1 + N ) ) )
112 1 17 110 4 111 syl22anc 
 |-  ( ph -> ( ( S Dn ( ( S Dn F ) ` 1 ) ) ` N ) = ( ( S Dn F ) ` ( 1 + N ) ) )
113 dvn1 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 1 ) = ( S _D F ) )
114 40 17 113 syl2anc 
 |-  ( ph -> ( ( S Dn F ) ` 1 ) = ( S _D F ) )
115 114 oveq2d 
 |-  ( ph -> ( S Dn ( ( S Dn F ) ` 1 ) ) = ( S Dn ( S _D F ) ) )
116 115 fveq1d 
 |-  ( ph -> ( ( S Dn ( ( S Dn F ) ` 1 ) ) ` N ) = ( ( S Dn ( S _D F ) ) ` N ) )
117 1cnd 
 |-  ( ph -> 1 e. CC )
118 4 nn0cnd 
 |-  ( ph -> N e. CC )
119 117 118 addcomd 
 |-  ( ph -> ( 1 + N ) = ( N + 1 ) )
120 119 fveq2d 
 |-  ( ph -> ( ( S Dn F ) ` ( 1 + N ) ) = ( ( S Dn F ) ` ( N + 1 ) ) )
121 112 116 120 3eqtr3d 
 |-  ( ph -> ( ( S Dn ( S _D F ) ) ` N ) = ( ( S Dn F ) ` ( N + 1 ) ) )
122 121 dmeqd 
 |-  ( ph -> dom ( ( S Dn ( S _D F ) ) ` N ) = dom ( ( S Dn F ) ` ( N + 1 ) ) )
123 5 122 eleqtrrd 
 |-  ( ph -> B e. dom ( ( S Dn ( S _D F ) ) ` N ) )
124 1 106 108 4 123 taylplem2 
 |-  ( ( ( ph /\ x e. CC ) /\ j e. ( 0 ... N ) ) -> ( ( ( ( ( S Dn ( S _D F ) ) ` j ) ` B ) / ( ! ` j ) ) x. ( ( x - B ) ^ j ) ) e. CC )
125 fveq2 
 |-  ( j = ( k - 1 ) -> ( ( S Dn ( S _D F ) ) ` j ) = ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) )
126 125 fveq1d 
 |-  ( j = ( k - 1 ) -> ( ( ( S Dn ( S _D F ) ) ` j ) ` B ) = ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) )
127 fveq2 
 |-  ( j = ( k - 1 ) -> ( ! ` j ) = ( ! ` ( k - 1 ) ) )
128 126 127 oveq12d 
 |-  ( j = ( k - 1 ) -> ( ( ( ( S Dn ( S _D F ) ) ` j ) ` B ) / ( ! ` j ) ) = ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) )
129 oveq2 
 |-  ( j = ( k - 1 ) -> ( ( x - B ) ^ j ) = ( ( x - B ) ^ ( k - 1 ) ) )
130 128 129 oveq12d 
 |-  ( j = ( k - 1 ) -> ( ( ( ( ( S Dn ( S _D F ) ) ` j ) ` B ) / ( ! ` j ) ) x. ( ( x - B ) ^ j ) ) = ( ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) x. ( ( x - B ) ^ ( k - 1 ) ) ) )
131 101 102 104 124 130 fsumshft 
 |-  ( ( ph /\ x e. CC ) -> sum_ j e. ( 0 ... N ) ( ( ( ( ( S Dn ( S _D F ) ) ` j ) ` B ) / ( ! ` j ) ) x. ( ( x - B ) ^ j ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) x. ( ( x - B ) ^ ( k - 1 ) ) ) )
132 elfznn 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. NN )
133 132 adantl 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> k e. NN )
134 133 nnne0d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> k =/= 0 )
135 ifnefalse 
 |-  ( k =/= 0 -> if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) = ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) )
136 134 135 syl 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) = ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) )
137 136 oveq2d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) )
138 simpll 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ph )
139 fz1ssfz0 
 |-  ( 1 ... ( N + 1 ) ) C_ ( 0 ... ( N + 1 ) )
140 139 sseli 
 |-  ( k e. ( 1 ... ( N + 1 ) ) -> k e. ( 0 ... ( N + 1 ) ) )
141 140 adantl 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> k e. ( 0 ... ( N + 1 ) ) )
142 138 141 36 syl2anc 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. CC )
143 133 nncnd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> k e. CC )
144 simplr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> x e. CC )
145 46 ad2antrr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> B e. CC )
146 144 145 subcld 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( x - B ) e. CC )
147 133 61 syl 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( k - 1 ) e. NN0 )
148 146 147 expcld 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( x - B ) ^ ( k - 1 ) ) e. CC )
149 142 143 148 mulassd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. k ) x. ( ( x - B ) ^ ( k - 1 ) ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) )
150 facp1 
 |-  ( ( k - 1 ) e. NN0 -> ( ! ` ( ( k - 1 ) + 1 ) ) = ( ( ! ` ( k - 1 ) ) x. ( ( k - 1 ) + 1 ) ) )
151 147 150 syl 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ! ` ( ( k - 1 ) + 1 ) ) = ( ( ! ` ( k - 1 ) ) x. ( ( k - 1 ) + 1 ) ) )
152 1cnd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> 1 e. CC )
153 143 152 npcand 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( k - 1 ) + 1 ) = k )
154 153 fveq2d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ! ` ( ( k - 1 ) + 1 ) ) = ( ! ` k ) )
155 153 oveq2d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ! ` ( k - 1 ) ) x. ( ( k - 1 ) + 1 ) ) = ( ( ! ` ( k - 1 ) ) x. k ) )
156 151 154 155 3eqtr3d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ! ` k ) = ( ( ! ` ( k - 1 ) ) x. k ) )
157 156 oveq2d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) x. k ) / ( ! ` k ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) x. k ) / ( ( ! ` ( k - 1 ) ) x. k ) ) )
158 32 nn0cnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. CC )
159 31 158 34 35 div23d 
 |-  ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) x. k ) / ( ! ` k ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. k ) )
160 138 141 159 syl2anc 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) x. k ) / ( ! ` k ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. k ) )
161 138 141 31 syl2anc 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( S Dn F ) ` k ) ` B ) e. CC )
162 147 faccld 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ! ` ( k - 1 ) ) e. NN )
163 162 nncnd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ! ` ( k - 1 ) ) e. CC )
164 162 nnne0d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ! ` ( k - 1 ) ) =/= 0 )
165 161 163 143 164 134 divcan5rd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) x. k ) / ( ( ! ` ( k - 1 ) ) x. k ) ) = ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` ( k - 1 ) ) ) )
166 1 ad2antrr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> S e. { RR , CC } )
167 17 ad2antrr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> F e. ( CC ^pm S ) )
168 109 a1i 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> 1 e. NN0 )
169 dvnadd 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( 1 e. NN0 /\ ( k - 1 ) e. NN0 ) ) -> ( ( S Dn ( ( S Dn F ) ` 1 ) ) ` ( k - 1 ) ) = ( ( S Dn F ) ` ( 1 + ( k - 1 ) ) ) )
170 166 167 168 147 169 syl22anc 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( S Dn ( ( S Dn F ) ` 1 ) ) ` ( k - 1 ) ) = ( ( S Dn F ) ` ( 1 + ( k - 1 ) ) ) )
171 114 ad2antrr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( S Dn F ) ` 1 ) = ( S _D F ) )
172 171 oveq2d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( S Dn ( ( S Dn F ) ` 1 ) ) = ( S Dn ( S _D F ) ) )
173 172 fveq1d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( S Dn ( ( S Dn F ) ` 1 ) ) ` ( k - 1 ) ) = ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) )
174 152 143 pncan3d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( 1 + ( k - 1 ) ) = k )
175 174 fveq2d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( S Dn F ) ` ( 1 + ( k - 1 ) ) ) = ( ( S Dn F ) ` k ) )
176 170 173 175 3eqtr3rd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( S Dn F ) ` k ) = ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) )
177 176 fveq1d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( S Dn F ) ` k ) ` B ) = ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) )
178 177 oveq1d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` ( k - 1 ) ) ) = ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) )
179 165 178 eqtrd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) x. k ) / ( ( ! ` ( k - 1 ) ) x. k ) ) = ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) )
180 157 160 179 3eqtr3d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. k ) = ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) )
181 180 oveq1d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. k ) x. ( ( x - B ) ^ ( k - 1 ) ) ) = ( ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) x. ( ( x - B ) ^ ( k - 1 ) ) ) )
182 137 149 181 3eqtr2d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) = ( ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) x. ( ( x - B ) ^ ( k - 1 ) ) ) )
183 182 sumeq2dv 
 |-  ( ( ph /\ x e. CC ) -> sum_ k e. ( 1 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) = sum_ k e. ( 1 ... ( N + 1 ) ) ( ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) x. ( ( x - B ) ^ ( k - 1 ) ) ) )
184 0p1e1 
 |-  ( 0 + 1 ) = 1
185 184 oveq1i 
 |-  ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) )
186 185 sumeq1i 
 |-  sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) x. ( ( x - B ) ^ ( k - 1 ) ) ) = sum_ k e. ( 1 ... ( N + 1 ) ) ( ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) x. ( ( x - B ) ^ ( k - 1 ) ) )
187 183 186 eqtr4di 
 |-  ( ( ph /\ x e. CC ) -> sum_ k e. ( 1 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( ( ( ( S Dn ( S _D F ) ) ` ( k - 1 ) ) ` B ) / ( ! ` ( k - 1 ) ) ) x. ( ( x - B ) ^ ( k - 1 ) ) ) )
188 139 a1i 
 |-  ( ( ph /\ x e. CC ) -> ( 1 ... ( N + 1 ) ) C_ ( 0 ... ( N + 1 ) ) )
189 69 an32s 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 0 ... ( N + 1 ) ) ) -> if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) e. CC )
190 140 189 sylan2 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) e. CC )
191 142 190 mulcld 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) e. CC )
192 eldif 
 |-  ( k e. ( ( 0 ... ( N + 1 ) ) \ ( 1 ... ( N + 1 ) ) ) <-> ( k e. ( 0 ... ( N + 1 ) ) /\ -. k e. ( 1 ... ( N + 1 ) ) ) )
193 59 biimpri 
 |-  ( ( k e. NN0 /\ k =/= 0 ) -> k e. NN )
194 18 193 sylan 
 |-  ( ( k e. ( 0 ... ( N + 1 ) ) /\ k =/= 0 ) -> k e. NN )
195 nnuz 
 |-  NN = ( ZZ>= ` 1 )
196 194 195 eleqtrdi 
 |-  ( ( k e. ( 0 ... ( N + 1 ) ) /\ k =/= 0 ) -> k e. ( ZZ>= ` 1 ) )
197 elfzuz3 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( N + 1 ) e. ( ZZ>= ` k ) )
198 197 adantr 
 |-  ( ( k e. ( 0 ... ( N + 1 ) ) /\ k =/= 0 ) -> ( N + 1 ) e. ( ZZ>= ` k ) )
199 elfzuzb 
 |-  ( k e. ( 1 ... ( N + 1 ) ) <-> ( k e. ( ZZ>= ` 1 ) /\ ( N + 1 ) e. ( ZZ>= ` k ) ) )
200 196 198 199 sylanbrc 
 |-  ( ( k e. ( 0 ... ( N + 1 ) ) /\ k =/= 0 ) -> k e. ( 1 ... ( N + 1 ) ) )
201 200 ex 
 |-  ( k e. ( 0 ... ( N + 1 ) ) -> ( k =/= 0 -> k e. ( 1 ... ( N + 1 ) ) ) )
202 201 adantl 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( k =/= 0 -> k e. ( 1 ... ( N + 1 ) ) ) )
203 202 necon1bd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -. k e. ( 1 ... ( N + 1 ) ) -> k = 0 ) )
204 203 impr 
 |-  ( ( ( ph /\ x e. CC ) /\ ( k e. ( 0 ... ( N + 1 ) ) /\ -. k e. ( 1 ... ( N + 1 ) ) ) ) -> k = 0 )
205 192 204 sylan2b 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 1 ... ( N + 1 ) ) ) ) -> k = 0 )
206 205 iftrued 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 1 ... ( N + 1 ) ) ) ) -> if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) = 0 )
207 206 oveq2d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 1 ... ( N + 1 ) ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. 0 ) )
208 eldifi 
 |-  ( k e. ( ( 0 ... ( N + 1 ) ) \ ( 1 ... ( N + 1 ) ) ) -> k e. ( 0 ... ( N + 1 ) ) )
209 36 adantlr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. CC )
210 208 209 sylan2 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 1 ... ( N + 1 ) ) ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. CC )
211 210 mul01d 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 1 ... ( N + 1 ) ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. 0 ) = 0 )
212 207 211 eqtrd 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. ( ( 0 ... ( N + 1 ) ) \ ( 1 ... ( N + 1 ) ) ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) = 0 )
213 fzfid 
 |-  ( ( ph /\ x e. CC ) -> ( 0 ... ( N + 1 ) ) e. Fin )
214 188 191 212 213 fsumss 
 |-  ( ( ph /\ x e. CC ) -> sum_ k e. ( 1 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) )
215 131 187 214 3eqtr2rd 
 |-  ( ( ph /\ x e. CC ) -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) = sum_ j e. ( 0 ... N ) ( ( ( ( ( S Dn ( S _D F ) ) ` j ) ` B ) / ( ! ` j ) ) x. ( ( x - B ) ^ j ) ) )
216 215 mpteq2dva 
 |-  ( ph -> ( x e. CC |-> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. if ( k = 0 , 0 , ( k x. ( ( x - B ) ^ ( k - 1 ) ) ) ) ) ) = ( x e. CC |-> sum_ j e. ( 0 ... N ) ( ( ( ( ( S Dn ( S _D F ) ) ` j ) ` B ) / ( ! ` j ) ) x. ( ( x - B ) ^ j ) ) ) )
217 100 216 eqtrd 
 |-  ( ph -> ( CC _D ( x e. CC |-> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) = ( x e. CC |-> sum_ j e. ( 0 ... N ) ( ( ( ( ( S Dn ( S _D F ) ) ` j ) ` B ) / ( ! ` j ) ) x. ( ( x - B ) ^ j ) ) ) )
218 eqid 
 |-  ( ( N + 1 ) ( S Tayl F ) B ) = ( ( N + 1 ) ( S Tayl F ) B )
219 1 2 3 23 5 218 taylpfval 
 |-  ( ph -> ( ( N + 1 ) ( S Tayl F ) B ) = ( x e. CC |-> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) )
220 219 oveq2d 
 |-  ( ph -> ( CC _D ( ( N + 1 ) ( S Tayl F ) B ) ) = ( CC _D ( x e. CC |-> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) )
221 eqid 
 |-  ( N ( S Tayl ( S _D F ) ) B ) = ( N ( S Tayl ( S _D F ) ) B )
222 1 106 108 4 123 221 taylpfval 
 |-  ( ph -> ( N ( S Tayl ( S _D F ) ) B ) = ( x e. CC |-> sum_ j e. ( 0 ... N ) ( ( ( ( ( S Dn ( S _D F ) ) ` j ) ` B ) / ( ! ` j ) ) x. ( ( x - B ) ^ j ) ) ) )
223 217 220 222 3eqtr4d 
 |-  ( ph -> ( CC _D ( ( N + 1 ) ( S Tayl F ) B ) ) = ( N ( S Tayl ( S _D F ) ) B ) )