# 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 ) )`
` |-  ( ( ( 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 ) )`