# Metamath Proof Explorer

## Theorem dvntaylp

Description: The M -th derivative of the Taylor polynomial is the Taylor polynomial of the M -th derivative of the function. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses dvntaylp.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
dvntaylp.f ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
dvntaylp.a ( 𝜑𝐴𝑆 )
dvntaylp.m ( 𝜑𝑀 ∈ ℕ0 )
dvntaylp.n ( 𝜑𝑁 ∈ ℕ0 )
dvntaylp.b ( 𝜑𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 𝑀 ) ) )
Assertion dvntaylp ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) = ( 𝑁 ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) )

### Proof

Step Hyp Ref Expression
1 dvntaylp.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
2 dvntaylp.f ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
3 dvntaylp.a ( 𝜑𝐴𝑆 )
4 dvntaylp.m ( 𝜑𝑀 ∈ ℕ0 )
5 dvntaylp.n ( 𝜑𝑁 ∈ ℕ0 )
6 dvntaylp.b ( 𝜑𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 𝑀 ) ) )
7 nn0uz 0 = ( ℤ ‘ 0 )
8 4 7 eleqtrdi ( 𝜑𝑀 ∈ ( ℤ ‘ 0 ) )
9 eluzfz2b ( 𝑀 ∈ ( ℤ ‘ 0 ) ↔ 𝑀 ∈ ( 0 ... 𝑀 ) )
10 8 9 sylib ( 𝜑𝑀 ∈ ( 0 ... 𝑀 ) )
11 fveq2 ( 𝑚 = 0 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 0 ) )
12 fveq2 ( 𝑚 = 0 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) )
13 12 oveq2d ( 𝑚 = 0 → ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) = ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) )
14 oveq2 ( 𝑚 = 0 → ( 𝑀𝑚 ) = ( 𝑀 − 0 ) )
15 14 oveq2d ( 𝑚 = 0 → ( 𝑁 + ( 𝑀𝑚 ) ) = ( 𝑁 + ( 𝑀 − 0 ) ) )
16 eqidd ( 𝑚 = 0 → 𝐵 = 𝐵 )
17 13 15 16 oveq123d ( 𝑚 = 0 → ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) = ( ( 𝑁 + ( 𝑀 − 0 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) 𝐵 ) )
18 11 17 eqeq12d ( 𝑚 = 0 → ( ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) ↔ ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 0 ) = ( ( 𝑁 + ( 𝑀 − 0 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) 𝐵 ) ) )
19 18 imbi2d ( 𝑚 = 0 → ( ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) ) ↔ ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 0 ) = ( ( 𝑁 + ( 𝑀 − 0 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) 𝐵 ) ) ) )
20 fveq2 ( 𝑚 = 𝑛 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) )
21 fveq2 ( 𝑚 = 𝑛 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) )
22 21 oveq2d ( 𝑚 = 𝑛 → ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) = ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) )
23 oveq2 ( 𝑚 = 𝑛 → ( 𝑀𝑚 ) = ( 𝑀𝑛 ) )
24 23 oveq2d ( 𝑚 = 𝑛 → ( 𝑁 + ( 𝑀𝑚 ) ) = ( 𝑁 + ( 𝑀𝑛 ) ) )
25 eqidd ( 𝑚 = 𝑛𝐵 = 𝐵 )
26 22 24 25 oveq123d ( 𝑚 = 𝑛 → ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) = ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) )
27 20 26 eqeq12d ( 𝑚 = 𝑛 → ( ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) ↔ ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) = ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) ) )
28 27 imbi2d ( 𝑚 = 𝑛 → ( ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) ) ↔ ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) = ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) ) ) )
29 fveq2 ( 𝑚 = ( 𝑛 + 1 ) → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) )
30 fveq2 ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
31 30 oveq2d ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) = ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
32 oveq2 ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑀𝑚 ) = ( 𝑀 − ( 𝑛 + 1 ) ) )
33 32 oveq2d ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑁 + ( 𝑀𝑚 ) ) = ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) )
34 eqidd ( 𝑚 = ( 𝑛 + 1 ) → 𝐵 = 𝐵 )
35 31 33 34 oveq123d ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) = ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) 𝐵 ) )
36 29 35 eqeq12d ( 𝑚 = ( 𝑛 + 1 ) → ( ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) ↔ ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) 𝐵 ) ) )
37 36 imbi2d ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) ) ↔ ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) 𝐵 ) ) ) )
38 fveq2 ( 𝑚 = 𝑀 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) )
39 fveq2 ( 𝑚 = 𝑀 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) )
40 39 oveq2d ( 𝑚 = 𝑀 → ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) = ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) )
41 oveq2 ( 𝑚 = 𝑀 → ( 𝑀𝑚 ) = ( 𝑀𝑀 ) )
42 41 oveq2d ( 𝑚 = 𝑀 → ( 𝑁 + ( 𝑀𝑚 ) ) = ( 𝑁 + ( 𝑀𝑀 ) ) )
43 eqidd ( 𝑚 = 𝑀𝐵 = 𝐵 )
44 40 42 43 oveq123d ( 𝑚 = 𝑀 → ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) = ( ( 𝑁 + ( 𝑀𝑀 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) )
45 38 44 eqeq12d ( 𝑚 = 𝑀 → ( ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) ↔ ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) = ( ( 𝑁 + ( 𝑀𝑀 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ) )
46 45 imbi2d ( 𝑚 = 𝑀 → ( ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑁 + ( 𝑀𝑚 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) 𝐵 ) ) ↔ ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) = ( ( 𝑁 + ( 𝑀𝑀 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ) ) )
47 ssidd ( 𝜑 → ℂ ⊆ ℂ )
48 mapsspm ( ℂ ↑m ℂ ) ⊆ ( ℂ ↑pm ℂ )
49 5 4 nn0addcld ( 𝜑 → ( 𝑁 + 𝑀 ) ∈ ℕ0 )
50 eqid ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) = ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 )
51 1 2 3 49 6 50 taylpf ( 𝜑 → ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) : ℂ ⟶ ℂ )
52 cnex ℂ ∈ V
53 52 52 elmap ( ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ∈ ( ℂ ↑m ℂ ) ↔ ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) : ℂ ⟶ ℂ )
54 51 53 sylibr ( 𝜑 → ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ∈ ( ℂ ↑m ℂ ) )
55 48 54 sseldi ( 𝜑 → ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ∈ ( ℂ ↑pm ℂ ) )
56 dvn0 ( ( ℂ ⊆ ℂ ∧ ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ∈ ( ℂ ↑pm ℂ ) ) → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 0 ) = ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) )
57 47 55 56 syl2anc ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 0 ) = ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) )
58 recnprss ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
59 1 58 syl ( 𝜑𝑆 ⊆ ℂ )
60 52 a1i ( 𝜑 → ℂ ∈ V )
61 elpm2r ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
62 60 1 2 3 61 syl22anc ( 𝜑𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
63 dvn0 ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
64 59 62 63 syl2anc ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
65 64 oveq2d ( 𝜑 → ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) = ( 𝑆 Tayl 𝐹 ) )
66 4 nn0cnd ( 𝜑𝑀 ∈ ℂ )
67 66 subid1d ( 𝜑 → ( 𝑀 − 0 ) = 𝑀 )
68 67 oveq2d ( 𝜑 → ( 𝑁 + ( 𝑀 − 0 ) ) = ( 𝑁 + 𝑀 ) )
69 eqidd ( 𝜑𝐵 = 𝐵 )
70 65 68 69 oveq123d ( 𝜑 → ( ( 𝑁 + ( 𝑀 − 0 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) 𝐵 ) = ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) )
71 57 70 eqtr4d ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 0 ) = ( ( 𝑁 + ( 𝑀 − 0 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) 𝐵 ) )
72 71 a1i ( 𝑀 ∈ ( ℤ ‘ 0 ) → ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 0 ) = ( ( 𝑁 + ( 𝑀 − 0 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ) 𝐵 ) ) )
73 oveq2 ( ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) = ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) → ( ℂ D ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) ) = ( ℂ D ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) ) )
74 ssidd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ℂ ⊆ ℂ )
75 55 adantr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ∈ ( ℂ ↑pm ℂ ) )
76 elfzouz ( 𝑛 ∈ ( 0 ..^ 𝑀 ) → 𝑛 ∈ ( ℤ ‘ 0 ) )
77 76 adantl ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝑛 ∈ ( ℤ ‘ 0 ) )
78 77 7 eleqtrrdi ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝑛 ∈ ℕ0 )
79 dvnp1 ( ( ℂ ⊆ ℂ ∧ ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ∈ ( ℂ ↑pm ℂ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) ) )
80 74 75 78 79 syl3anc ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ℂ D ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) ) )
81 1 adantr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝑆 ∈ { ℝ , ℂ } )
82 62 adantr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
83 dvnf ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ⟶ ℂ )
84 81 82 78 83 syl3anc ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ⟶ ℂ )
85 dvnbss ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ⊆ dom 𝐹 )
86 81 82 78 85 syl3anc ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ⊆ dom 𝐹 )
87 2 fdmd ( 𝜑 → dom 𝐹 = 𝐴 )
88 87 adantr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → dom 𝐹 = 𝐴 )
89 86 88 sseqtrd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ⊆ 𝐴 )
90 3 adantr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴𝑆 )
91 89 90 sstrd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ⊆ 𝑆 )
92 5 adantr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝑁 ∈ ℕ0 )
93 fzofzp1 ( 𝑛 ∈ ( 0 ..^ 𝑀 ) → ( 𝑛 + 1 ) ∈ ( 0 ... 𝑀 ) )
94 93 adantl ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑛 + 1 ) ∈ ( 0 ... 𝑀 ) )
95 fznn0sub ( ( 𝑛 + 1 ) ∈ ( 0 ... 𝑀 ) → ( 𝑀 − ( 𝑛 + 1 ) ) ∈ ℕ0 )
96 94 95 syl ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑀 − ( 𝑛 + 1 ) ) ∈ ℕ0 )
97 92 96 nn0addcld ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ∈ ℕ0 )
98 6 adantr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 𝑀 ) ) )
99 elfzofz ( 𝑛 ∈ ( 0 ..^ 𝑀 ) → 𝑛 ∈ ( 0 ... 𝑀 ) )
100 99 adantl ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝑛 ∈ ( 0 ... 𝑀 ) )
101 fznn0sub ( 𝑛 ∈ ( 0 ... 𝑀 ) → ( 𝑀𝑛 ) ∈ ℕ0 )
102 100 101 syl ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑀𝑛 ) ∈ ℕ0 )
103 92 102 nn0addcld ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑁 + ( 𝑀𝑛 ) ) ∈ ℕ0 )
104 dvnadd ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑁 + ( 𝑀𝑛 ) ) ∈ ℕ0 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ‘ ( 𝑁 + ( 𝑀𝑛 ) ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + ( 𝑁 + ( 𝑀𝑛 ) ) ) ) )
105 81 82 78 103 104 syl22anc ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ‘ ( 𝑁 + ( 𝑀𝑛 ) ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + ( 𝑁 + ( 𝑀𝑛 ) ) ) ) )
106 5 nn0cnd ( 𝜑𝑁 ∈ ℂ )
107 106 adantr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝑁 ∈ ℂ )
108 96 nn0cnd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑀 − ( 𝑛 + 1 ) ) ∈ ℂ )
109 1cnd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 1 ∈ ℂ )
110 107 108 109 addassd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) + 1 ) = ( 𝑁 + ( ( 𝑀 − ( 𝑛 + 1 ) ) + 1 ) ) )
111 66 adantr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝑀 ∈ ℂ )
112 78 nn0cnd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝑛 ∈ ℂ )
113 111 112 109 nppcan2d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑀 − ( 𝑛 + 1 ) ) + 1 ) = ( 𝑀𝑛 ) )
114 113 oveq2d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑁 + ( ( 𝑀 − ( 𝑛 + 1 ) ) + 1 ) ) = ( 𝑁 + ( 𝑀𝑛 ) ) )
115 110 114 eqtrd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) + 1 ) = ( 𝑁 + ( 𝑀𝑛 ) ) )
116 115 fveq2d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ‘ ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) + 1 ) ) = ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ‘ ( 𝑁 + ( 𝑀𝑛 ) ) ) )
117 112 111 pncan3d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑛 + ( 𝑀𝑛 ) ) = 𝑀 )
118 117 oveq2d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑁 + ( 𝑛 + ( 𝑀𝑛 ) ) ) = ( 𝑁 + 𝑀 ) )
119 111 112 subcld ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑀𝑛 ) ∈ ℂ )
120 107 112 119 add12d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑁 + ( 𝑛 + ( 𝑀𝑛 ) ) ) = ( 𝑛 + ( 𝑁 + ( 𝑀𝑛 ) ) ) )
121 118 120 eqtr3d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑁 + 𝑀 ) = ( 𝑛 + ( 𝑁 + ( 𝑀𝑛 ) ) ) )
122 121 fveq2d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 𝑀 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + ( 𝑁 + ( 𝑀𝑛 ) ) ) ) )
123 105 116 122 3eqtr4d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ‘ ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) + 1 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 𝑀 ) ) )
124 123 dmeqd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ‘ ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) + 1 ) ) = dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 𝑀 ) ) )
125 98 124 eleqtrrd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ‘ ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) + 1 ) ) )
126 81 84 91 97 125 dvtaylp ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ℂ D ( ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) + 1 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) ) = ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ) 𝐵 ) )
127 115 oveq1d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) + 1 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) = ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) )
128 127 oveq2d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ℂ D ( ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) + 1 ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) ) = ( ℂ D ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) ) )
129 59 adantr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → 𝑆 ⊆ ℂ )
130 dvnp1 ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) )
131 129 82 78 130 syl3anc ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) )
132 131 oveq2d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( 𝑆 Tayl ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ) )
133 132 eqcomd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 Tayl ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ) = ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
134 133 oveqd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) ) 𝐵 ) = ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) 𝐵 ) )
135 126 128 134 3eqtr3rd ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) 𝐵 ) = ( ℂ D ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) ) )
136 80 135 eqeq12d ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) 𝐵 ) ↔ ( ℂ D ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) ) = ( ℂ D ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) ) ) )
137 73 136 syl5ibr ( ( 𝜑𝑛 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) = ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) 𝐵 ) ) )
138 137 expcom ( 𝑛 ∈ ( 0 ..^ 𝑀 ) → ( 𝜑 → ( ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) = ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) 𝐵 ) ) ) )
139 138 a2d ( 𝑛 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑛 ) = ( ( 𝑁 + ( 𝑀𝑛 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) ) 𝐵 ) ) → ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( 𝑁 + ( 𝑀 − ( 𝑛 + 1 ) ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) 𝐵 ) ) ) )
140 19 28 37 46 72 139 fzind2 ( 𝑀 ∈ ( 0 ... 𝑀 ) → ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) = ( ( 𝑁 + ( 𝑀𝑀 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) ) )
141 10 140 mpcom ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) = ( ( 𝑁 + ( 𝑀𝑀 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) )
142 66 subidd ( 𝜑 → ( 𝑀𝑀 ) = 0 )
143 142 oveq2d ( 𝜑 → ( 𝑁 + ( 𝑀𝑀 ) ) = ( 𝑁 + 0 ) )
144 106 addid1d ( 𝜑 → ( 𝑁 + 0 ) = 𝑁 )
145 143 144 eqtrd ( 𝜑 → ( 𝑁 + ( 𝑀𝑀 ) ) = 𝑁 )
146 145 oveq1d ( 𝜑 → ( ( 𝑁 + ( 𝑀𝑀 ) ) ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) = ( 𝑁 ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) )
147 141 146 eqtrd ( 𝜑 → ( ( ℂ D𝑛 ( ( 𝑁 + 𝑀 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) ‘ 𝑀 ) = ( 𝑁 ( 𝑆 Tayl ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) )