Metamath Proof Explorer

Theorem dvntaylp0

Description: The first N derivatives of the Taylor polynomial at B match the derivatives of the function from which it is derived. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses dvntaylp0.s 
|- ( ph -> S e. { RR , CC } )
dvntaylp0.f 
|- ( ph -> F : A --> CC )
dvntaylp0.a 
|- ( ph -> A C_ S )
dvntaylp0.m 
|- ( ph -> M e. ( 0 ... N ) )
dvntaylp0.b 
|- ( ph -> B e. dom ( ( S Dn F ) ` N ) )
dvntaylp0.t 
|- T = ( N ( S Tayl F ) B )
Assertion dvntaylp0 
|- ( ph -> ( ( ( CC Dn T ) ` M ) ` B ) = ( ( ( S Dn F ) ` M ) ` B ) )

Proof

Step Hyp Ref Expression
1 dvntaylp0.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvntaylp0.f 
 |-  ( ph -> F : A --> CC )
3 dvntaylp0.a 
 |-  ( ph -> A C_ S )
4 dvntaylp0.m 
 |-  ( ph -> M e. ( 0 ... N ) )
5 dvntaylp0.b 
 |-  ( ph -> B e. dom ( ( S Dn F ) ` N ) )
6 dvntaylp0.t 
 |-  T = ( N ( S Tayl F ) B )
7 elfz3nn0 
 |-  ( M e. ( 0 ... N ) -> N e. NN0 )
8 4 7 syl 
 |-  ( ph -> N e. NN0 )
9 8 nn0cnd 
 |-  ( ph -> N e. CC )
10 elfznn0 
 |-  ( M e. ( 0 ... N ) -> M e. NN0 )
11 4 10 syl 
 |-  ( ph -> M e. NN0 )
12 11 nn0cnd 
 |-  ( ph -> M e. CC )
13 9 12 npcand 
 |-  ( ph -> ( ( N - M ) + M ) = N )
14 13 oveq1d 
 |-  ( ph -> ( ( ( N - M ) + M ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
15 14 6 eqtr4di 
 |-  ( ph -> ( ( ( N - M ) + M ) ( S Tayl F ) B ) = T )
16 15 oveq2d 
 |-  ( ph -> ( CC Dn ( ( ( N - M ) + M ) ( S Tayl F ) B ) ) = ( CC Dn T ) )
17 16 fveq1d 
 |-  ( ph -> ( ( CC Dn ( ( ( N - M ) + M ) ( S Tayl F ) B ) ) ` M ) = ( ( CC Dn T ) ` M ) )
18 fznn0sub 
 |-  ( M e. ( 0 ... N ) -> ( N - M ) e. NN0 )
19 4 18 syl 
 |-  ( ph -> ( N - M ) e. NN0 )
20 13 fveq2d 
 |-  ( ph -> ( ( S Dn F ) ` ( ( N - M ) + M ) ) = ( ( S Dn F ) ` N ) )
21 20 dmeqd 
 |-  ( ph -> dom ( ( S Dn F ) ` ( ( N - M ) + M ) ) = dom ( ( S Dn F ) ` N ) )
22 5 21 eleqtrrd 
 |-  ( ph -> B e. dom ( ( S Dn F ) ` ( ( N - M ) + M ) ) )
23 1 2 3 11 19 22 dvntaylp 
 |-  ( ph -> ( ( CC Dn ( ( ( N - M ) + M ) ( S Tayl F ) B ) ) ` M ) = ( ( N - M ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) )
24 17 23 eqtr3d 
 |-  ( ph -> ( ( CC Dn T ) ` M ) = ( ( N - M ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) )
25 24 fveq1d 
 |-  ( ph -> ( ( ( CC Dn T ) ` M ) ` B ) = ( ( ( N - M ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) ` B ) )
26 cnex 
 |-  CC e. _V
27 26 a1i 
 |-  ( ph -> CC e. _V )
28 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
29 27 1 2 3 28 syl22anc 
 |-  ( ph -> F e. ( CC ^pm S ) )
30 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. NN0 ) -> ( ( S Dn F ) ` M ) : dom ( ( S Dn F ) ` M ) --> CC )
31 1 29 11 30 syl3anc 
 |-  ( ph -> ( ( S Dn F ) ` M ) : dom ( ( S Dn F ) ` M ) --> CC )
32 dvnbss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. NN0 ) -> dom ( ( S Dn F ) ` M ) C_ dom F )
33 1 29 11 32 syl3anc 
 |-  ( ph -> dom ( ( S Dn F ) ` M ) C_ dom F )
34 2 33 fssdmd 
 |-  ( ph -> dom ( ( S Dn F ) ` M ) C_ A )
35 34 3 sstrd 
 |-  ( ph -> dom ( ( S Dn F ) ` M ) C_ S )
36 19 orcd 
 |-  ( ph -> ( ( N - M ) e. NN0 \/ ( N - M ) = +oo ) )
37 dvnadd 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( M e. NN0 /\ ( N - M ) e. NN0 ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) = ( ( S Dn F ) ` ( M + ( N - M ) ) ) )
38 1 29 11 19 37 syl22anc 
 |-  ( ph -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) = ( ( S Dn F ) ` ( M + ( N - M ) ) ) )
39 12 9 pncan3d 
 |-  ( ph -> ( M + ( N - M ) ) = N )
40 39 fveq2d 
 |-  ( ph -> ( ( S Dn F ) ` ( M + ( N - M ) ) ) = ( ( S Dn F ) ` N ) )
41 38 40 eqtrd 
 |-  ( ph -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) = ( ( S Dn F ) ` N ) )
42 41 dmeqd 
 |-  ( ph -> dom ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) = dom ( ( S Dn F ) ` N ) )
43 5 42 eleqtrrd 
 |-  ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` M ) ) ` ( N - M ) ) )
44 1 31 35 19 43 taylplem1 
 |-  ( ( ph /\ k e. ( ( 0 [,] ( N - M ) ) i^i ZZ ) ) -> B e. dom ( ( S Dn ( ( S Dn F ) ` M ) ) ` k ) )
45 eqid 
 |-  ( ( N - M ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) = ( ( N - M ) ( S Tayl ( ( S Dn F ) ` M ) ) B )
46 1 31 35 36 44 45 tayl0 
 |-  ( ph -> ( B e. dom ( ( N - M ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) /\ ( ( ( N - M ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) ` B ) = ( ( ( S Dn F ) ` M ) ` B ) ) )
47 46 simprd 
 |-  ( ph -> ( ( ( N - M ) ( S Tayl ( ( S Dn F ) ` M ) ) B ) ` B ) = ( ( ( S Dn F ) ` M ) ` B ) )
48 25 47 eqtrd 
 |-  ( ph -> ( ( ( CC Dn T ) ` M ) ` B ) = ( ( ( S Dn F ) ` M ) ` B ) )