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𝑛 𝐹 ) ‘ 𝑀 ) ) 𝐵 ) )