Metamath Proof Explorer

Theorem dvtaylp

Description: The derivative of the Taylor polynomial is the Taylor polynomial of the derivative of the function. (Contributed by Mario Carneiro, 31-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 dvtaylp.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvtaylp.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3 dvtaylp.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4 dvtaylp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 dvtaylp.b ⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) )
6 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
7 6 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
8 7 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
9 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
10 9 a1i ⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
11 toponmax ⊢ ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) → ℂ ∈ ( TopOpen ‘ ℂfld ) )
12 7 11 mp1i ⊢ ( 𝜑 → ℂ ∈ ( TopOpen ‘ ℂfld ) )
13 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) ∈ Fin )
14 cnex ⊢ ℂ ∈ V
15 14 a1i ⊢ ( 𝜑 → ℂ ∈ V )
16 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
17 15 1 2 3 16 syl22anc ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
18 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ0 )
19 dvnf ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
20 1 17 18 19 syl2an3an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
21 0z ⊢ 0 ∈ ℤ
22 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
23 4 22 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
24 23 nn0zd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
25 fzval2 ⊢ ( ( 0 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 0 ... ( 𝑁 + 1 ) ) = ( ( 0 [,] ( 𝑁 + 1 ) ) ∩ ℤ ) )
26 21 24 25 sylancr ⊢ ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) = ( ( 0 [,] ( 𝑁 + 1 ) ) ∩ ℤ ) )
27 26 eleq2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↔ 𝑘 ∈ ( ( 0 [,] ( 𝑁 + 1 ) ) ∩ ℤ ) ) )
28 27 biimpa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ( ( 0 [,] ( 𝑁 + 1 ) ) ∩ ℤ ) )
29 1 2 3 23 5 taylplem1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 [,] ( 𝑁 + 1 ) ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
30 28 29 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
31 20 30 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) ∈ ℂ )
32 18 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
33 32 faccld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
34 33 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
35 33 nnne0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ! ‘ 𝑘 ) ≠ 0 )
36 31 34 35 divcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
37 36 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
38 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
39 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
40 1 39 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
41 3 40 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
42 dvnbss ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) ⊆ dom 𝐹 )
43 1 17 23 42 syl3anc ⊢ ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) ⊆ dom 𝐹 )
44 2 43 fssdmd ⊢ ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) ⊆ 𝐴 )
45 44 5 sseldd ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
46 41 45 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
47 46 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ℂ )
48 38 47 subcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) → ( 𝑥 − 𝐵 ) ∈ ℂ )
49 18 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) → 𝑘 ∈ ℕ0 )
50 48 49 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ∈ ℂ )
51 37 50 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )
52 0cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 = 0 ) → 0 ∈ ℂ )
53 49 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) → 𝑘 ∈ ℂ )
54 53 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → 𝑘 ∈ ℂ )
55 48 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → ( 𝑥 − 𝐵 ) ∈ ℂ )
56 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → 𝑘 ∈ ℕ0 )
57 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → ¬ 𝑘 = 0 )
58 57 neqned ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → 𝑘 ≠ 0 )
59 elnnne0 ⊢ ( 𝑘 ∈ ℕ ↔ ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≠ 0 ) )
60 56 58 59 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → 𝑘 ∈ ℕ )
61 nnm1nn0 ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 − 1 ) ∈ ℕ0 )
62 60 61 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → ( 𝑘 − 1 ) ∈ ℕ0 )
63 55 62 expcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
64 54 63 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ∈ ℂ )
65 52 64 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ∈ ℂ )
66 37 65 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ℂ ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) ∈ ℂ )
67 9 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ℂ ∈ { ℝ , ℂ } )
68 50 3expa ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ∈ ℂ )
69 65 3expa ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑥 ∈ ℂ ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ∈ ℂ )
70 48 3expa ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑥 ∈ ℂ ) → ( 𝑥 − 𝐵 ) ∈ ℂ )
71 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ )
72 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
73 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑦 ∈ ℂ ) → 𝑘 ∈ ℕ0 )
74 72 73 expcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ 𝑘 ) ∈ ℂ )
75 c0ex ⊢ 0 ∈ V
76 ovex ⊢ ( 𝑘 · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ∈ V
77 75 76 ifex ⊢ if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) ∈ V
78 77 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑦 ∈ ℂ ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) ∈ V )
79 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
80 67 dvmptid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) )
81 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ℂ )
82 0cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑥 ∈ ℂ ) → 0 ∈ ℂ )
83 46 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ ℂ )
84 67 83 dvmptc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝐵 ) ) = ( 𝑥 ∈ ℂ ↦ 0 ) )
85 67 79 71 80 81 82 84 dvmptsub ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 − 𝐵 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 1 − 0 ) ) )
86 1m0e1 ⊢ ( 1 − 0 ) = 1
87 86 mpteq2i ⊢ ( 𝑥 ∈ ℂ ↦ ( 1 − 0 ) ) = ( 𝑥 ∈ ℂ ↦ 1 )
88 85 87 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 − 𝐵 ) ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) )
89 dvexp2 ⊢ ( 𝑘 ∈ ℕ0 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ ℂ ↦ if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) ) )
90 32 89 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ ℂ ↦ if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) ) )
91 oveq1 ⊢ ( 𝑦 = ( 𝑥 − 𝐵 ) → ( 𝑦 ↑ 𝑘 ) = ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) )
92 oveq1 ⊢ ( 𝑦 = ( 𝑥 − 𝐵 ) → ( 𝑦 ↑ ( 𝑘 − 1 ) ) = ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) )
93 92 oveq2d ⊢ ( 𝑦 = ( 𝑥 − 𝐵 ) → ( 𝑘 · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) = ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) )
94 93 ifeq2d ⊢ ( 𝑦 = ( 𝑥 − 𝐵 ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) = if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) )
95 67 67 70 71 74 78 88 90 91 94 dvmptco ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) · 1 ) ) )
96 69 mulridd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ∧ 𝑥 ∈ ℂ ) → ( if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) · 1 ) = if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) )
97 96 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑥 ∈ ℂ ↦ ( if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) · 1 ) ) = ( 𝑥 ∈ ℂ ↦ if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) )
98 95 97 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) = ( 𝑥 ∈ ℂ ↦ if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) )
99 67 68 69 98 36 dvmptcmul ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) ) )
100 8 6 10 12 13 51 66 99 dvmptfsum ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) ) )
101 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℤ )
102 0zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 0 ∈ ℤ )
103 4 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
104 103 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑁 ∈ ℤ )
105 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
106 1 105 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
107 40 2 3 dvbss ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ 𝐴 )
108 107 3 sstrd ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ 𝑆 )
109 1nn0 ⊢ 1 ∈ ℕ0
110 109 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
111 dvnadd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 1 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 1 + 𝑁 ) ) )
112 1 17 110 4 111 syl22anc ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 1 + 𝑁 ) ) )
113 dvn1 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) = ( 𝑆 D 𝐹 ) )
114 40 17 113 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) = ( 𝑆 D 𝐹 ) )
115 114 oveq2d ⊢ ( 𝜑 → ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) ) = ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) )
116 115 fveq1d ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑁 ) )
117 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
118 4 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
119 117 118 addcomd ⊢ ( 𝜑 → ( 1 + 𝑁 ) = ( 𝑁 + 1 ) )
120 119 fveq2d ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 1 + 𝑁 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) )
121 112 116 120 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑁 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) )
122 121 dmeqd ⊢ ( 𝜑 → dom ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑁 ) = dom ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) )
123 5 122 eleqtrrd ⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑁 ) )
124 1 106 108 4 123 taylplem2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑗 ) ‘ 𝐵 ) / ( ! ‘ 𝑗 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑗 ) ) ∈ ℂ )
125 fveq2 ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) )
126 125 fveq1d ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑗 ) ‘ 𝐵 ) = ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) )
127 fveq2 ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ! ‘ 𝑗 ) = ( ! ‘ ( 𝑘 − 1 ) ) )
128 126 127 oveq12d ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑗 ) ‘ 𝐵 ) / ( ! ‘ 𝑗 ) ) = ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) )
129 oveq2 ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( 𝑥 − 𝐵 ) ↑ 𝑗 ) = ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) )
130 128 129 oveq12d ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑗 ) ‘ 𝐵 ) / ( ! ‘ 𝑗 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑗 ) ) = ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) )
131 101 102 104 124 130 fsumshft ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑗 ) ‘ 𝐵 ) / ( ! ‘ 𝑗 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑗 ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) )
132 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℕ )
133 132 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ )
134 133 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑘 ≠ 0 )
135 ifnefalse ⊢ ( 𝑘 ≠ 0 → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) = ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) )
136 134 135 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) = ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) )
137 136 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) )
138 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝜑 )
139 fz1ssfz0 ⊢ ( 1 ... ( 𝑁 + 1 ) ) ⊆ ( 0 ... ( 𝑁 + 1 ) )
140 139 sseli ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
141 140 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
142 138 141 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
143 133 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℂ )
144 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑥 ∈ ℂ )
145 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐵 ∈ ℂ )
146 144 145 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑥 − 𝐵 ) ∈ ℂ )
147 133 61 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℕ0 )
148 146 147 expcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
149 142 143 148 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · 𝑘 ) · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) )
150 facp1 ⊢ ( ( 𝑘 − 1 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑘 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑘 − 1 ) ) · ( ( 𝑘 − 1 ) + 1 ) ) )
151 147 150 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ! ‘ ( ( 𝑘 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑘 − 1 ) ) · ( ( 𝑘 − 1 ) + 1 ) ) )
152 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 1 ∈ ℂ )
153 143 152 npcand ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
154 153 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ! ‘ ( ( 𝑘 − 1 ) + 1 ) ) = ( ! ‘ 𝑘 ) )
155 153 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ! ‘ ( 𝑘 − 1 ) ) · ( ( 𝑘 − 1 ) + 1 ) ) = ( ( ! ‘ ( 𝑘 − 1 ) ) · 𝑘 ) )
156 151 154 155 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ! ‘ 𝑘 ) = ( ( ! ‘ ( 𝑘 − 1 ) ) · 𝑘 ) )
157 156 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) · 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) · 𝑘 ) / ( ( ! ‘ ( 𝑘 − 1 ) ) · 𝑘 ) ) )
158 32 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℂ )
159 31 158 34 35 div23d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) · 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · 𝑘 ) )
160 138 141 159 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) · 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · 𝑘 ) )
161 138 141 31 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) ∈ ℂ )
162 147 faccld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ! ‘ ( 𝑘 − 1 ) ) ∈ ℕ )
163 162 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ! ‘ ( 𝑘 − 1 ) ) ∈ ℂ )
164 162 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ! ‘ ( 𝑘 − 1 ) ) ≠ 0 )
165 161 163 143 164 134 divcan5rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) · 𝑘 ) / ( ( ! ‘ ( 𝑘 − 1 ) ) · 𝑘 ) ) = ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) )
166 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑆 ∈ { ℝ , ℂ } )
167 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
168 109 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 1 ∈ ℕ0 )
169 dvnadd ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 1 ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℕ0 ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) ) ‘ ( 𝑘 − 1 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 1 + ( 𝑘 − 1 ) ) ) )
170 166 167 168 147 169 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) ) ‘ ( 𝑘 − 1 ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 1 + ( 𝑘 − 1 ) ) ) )
171 114 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) = ( 𝑆 D 𝐹 ) )
172 171 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) ) = ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) )
173 172 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑆 D𝑛 ( ( 𝑆 D𝑛 𝐹 ) ‘ 1 ) ) ‘ ( 𝑘 − 1 ) ) = ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) )
174 152 143 pncan3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 1 + ( 𝑘 − 1 ) ) = 𝑘 )
175 174 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 1 + ( 𝑘 − 1 ) ) ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
176 170 173 175 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) )
177 176 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) = ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) )
178 177 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) = ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) )
179 165 178 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) · 𝑘 ) / ( ( ! ‘ ( 𝑘 − 1 ) ) · 𝑘 ) ) = ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) )
180 157 160 179 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · 𝑘 ) = ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) )
181 180 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · 𝑘 ) · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) = ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) )
182 137 149 181 3eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) = ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) )
183 182 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) = Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) )
184 0p1e1 ⊢ ( 0 + 1 ) = 1
185 184 oveq1i ⊢ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) = ( 1 ... ( 𝑁 + 1 ) )
186 185 sumeq1i ⊢ Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) )
187 183 186 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ ( 𝑘 − 1 ) ) ‘ 𝐵 ) / ( ! ‘ ( 𝑘 − 1 ) ) ) · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) )
188 139 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 1 ... ( 𝑁 + 1 ) ) ⊆ ( 0 ... ( 𝑁 + 1 ) ) )
189 69 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ∈ ℂ )
190 140 189 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ∈ ℂ )
191 142 190 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) ∈ ℂ )
192 eldif ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 1 ... ( 𝑁 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ ¬ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
193 59 biimpri ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑘 ≠ 0 ) → 𝑘 ∈ ℕ )
194 18 193 sylan ⊢ ( ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑘 ≠ 0 ) → 𝑘 ∈ ℕ )
195 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
196 194 195 eleqtrdi ⊢ ( ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑘 ≠ 0 ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
197 elfzuz3 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑘 ) )
198 197 adantr ⊢ ( ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑘 ≠ 0 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑘 ) )
199 elfzuzb ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) )
200 196 198 199 sylanbrc ⊢ ( ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ 𝑘 ≠ 0 ) → 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
201 200 ex ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑘 ≠ 0 → 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
202 201 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑘 ≠ 0 → 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
203 202 necon1bd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ¬ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑘 = 0 ) )
204 203 impr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ ¬ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) ) → 𝑘 = 0 )
205 192 204 sylan2b ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 1 ... ( 𝑁 + 1 ) ) ) ) → 𝑘 = 0 )
206 205 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 1 ... ( 𝑁 + 1 ) ) ) ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) = 0 )
207 206 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 1 ... ( 𝑁 + 1 ) ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · 0 ) )
208 eldifi ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
209 36 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
210 208 209 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 1 ... ( 𝑁 + 1 ) ) ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
211 210 mul01d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 1 ... ( 𝑁 + 1 ) ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · 0 ) = 0 )
212 207 211 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 + 1 ) ) ∖ ( 1 ... ( 𝑁 + 1 ) ) ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) = 0 )
213 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 0 ... ( 𝑁 + 1 ) ) ∈ Fin )
214 188 191 212 213 fsumss ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) )
215 131 187 214 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) = Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑗 ) ‘ 𝐵 ) / ( ! ‘ 𝑗 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑗 ) ) )
216 215 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( ( 𝑥 − 𝐵 ) ↑ ( 𝑘 − 1 ) ) ) ) ) ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑗 ) ‘ 𝐵 ) / ( ! ‘ 𝑗 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑗 ) ) ) )
217 100 216 eqtrd ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑗 ) ‘ 𝐵 ) / ( ! ‘ 𝑗 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑗 ) ) ) )
218 eqid ⊢ ( ( 𝑁 + 1 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) = ( ( 𝑁 + 1 ) ( 𝑆 Tayl 𝐹 ) 𝐵 )
219 1 2 3 23 5 218 taylpfval ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) )
220 219 oveq2d ⊢ ( 𝜑 → ( ℂ D ( ( 𝑁 + 1 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) )
221 eqid ⊢ ( 𝑁 ( 𝑆 Tayl ( 𝑆 D 𝐹 ) ) 𝐵 ) = ( 𝑁 ( 𝑆 Tayl ( 𝑆 D 𝐹 ) ) 𝐵 )
222 1 106 108 4 123 221 taylpfval ⊢ ( 𝜑 → ( 𝑁 ( 𝑆 Tayl ( 𝑆 D 𝐹 ) ) 𝐵 ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 ( 𝑆 D 𝐹 ) ) ‘ 𝑗 ) ‘ 𝐵 ) / ( ! ‘ 𝑗 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑗 ) ) ) )
223 217 220 222 3eqtr4d ⊢ ( 𝜑 → ( ℂ D ( ( 𝑁 + 1 ) ( 𝑆 Tayl 𝐹 ) 𝐵 ) ) = ( 𝑁 ( 𝑆 Tayl ( 𝑆 D 𝐹 ) ) 𝐵 ) )