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 φ S
dvntaylp0.f φ F : A
dvntaylp0.a φ A S
dvntaylp0.m φ M 0 N
dvntaylp0.b φ B dom S D n F N
dvntaylp0.t T = N S Tayl F B
Assertion dvntaylp0 φ D n T M B = S D n F M B

Proof

Step Hyp Ref Expression
1 dvntaylp0.s φ S
2 dvntaylp0.f φ F : A
3 dvntaylp0.a φ A S
4 dvntaylp0.m φ M 0 N
5 dvntaylp0.b φ B dom S D n F N
6 dvntaylp0.t T = N S Tayl F B
7 elfz3nn0 M 0 N N 0
8 4 7 syl φ N 0
9 8 nn0cnd φ N
10 elfznn0 M 0 N M 0
11 4 10 syl φ M 0
12 11 nn0cnd φ M
13 9 12 npcand φ N - M + M = N
14 13 oveq1d φ N - M + M S Tayl F B = N S Tayl F B
15 14 6 syl6eqr φ N - M + M S Tayl F B = T
16 15 oveq2d φ D n N - M + M S Tayl F B = D n T
17 16 fveq1d φ D n N - M + M S Tayl F B M = D n T M
18 fznn0sub M 0 N N M 0
19 4 18 syl φ N M 0
20 13 fveq2d φ S D n F N - M + M = S D n F N
21 20 dmeqd φ dom S D n F N - M + M = dom S D n F N
22 5 21 eleqtrrd φ B dom S D n F N - M + M
23 1 2 3 11 19 22 dvntaylp φ D n N - M + M S Tayl F B M = N M S Tayl S D n F M B
24 17 23 eqtr3d φ D n T M = N M S Tayl S D n F M B
25 24 fveq1d φ D n T M B = N M S Tayl S D n F M B B
26 cnex V
27 26 a1i φ V
28 elpm2r V S F : A A S F 𝑝𝑚 S
29 27 1 2 3 28 syl22anc φ F 𝑝𝑚 S
30 dvnf S F 𝑝𝑚 S M 0 S D n F M : dom S D n F M
31 1 29 11 30 syl3anc φ S D n F M : dom S D n F M
32 dvnbss S F 𝑝𝑚 S M 0 dom S D n F M dom F
33 1 29 11 32 syl3anc φ dom S D n F M dom F
34 2 33 fssdmd φ dom S D n F M A
35 34 3 sstrd φ dom S D n F M S
36 19 orcd φ N M 0 N M = +∞
37 dvnadd S F 𝑝𝑚 S M 0 N M 0 S D n S D n F M N M = S D n F M + N - M
38 1 29 11 19 37 syl22anc φ S D n S D n F M N M = S D n F M + N - M
39 12 9 pncan3d φ M + N - M = N
40 39 fveq2d φ S D n F M + N - M = S D n F N
41 38 40 eqtrd φ S D n S D n F M N M = S D n F N
42 41 dmeqd φ dom S D n S D n F M N M = dom S D n F N
43 5 42 eleqtrrd φ B dom S D n S D n F M N M
44 1 31 35 19 43 taylplem1 φ k 0 N M B dom S D n S D n F M k
45 eqid N M S Tayl S D n F M B = N M S Tayl S D n F M B
46 1 31 35 36 44 45 tayl0 φ B dom N M S Tayl S D n F M B N M S Tayl S D n F M B B = S D n F M B
47 46 simprd φ N M S Tayl S D n F M B B = S D n F M B
48 25 47 eqtrd φ D n T M B = S D n F M B