MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvtaylp Structured version   Visualization version   GIF version

Theorem dvtaylp 24429
Description: The derivative of the Taylor polynomial is the Taylor polynomial of the derivative of the function. (Contributed by Mario Carneiro, 31-Dec-2016.)
Hypotheses
Ref Expression
dvtaylp.s (𝜑𝑆 ∈ {ℝ, ℂ})
dvtaylp.f (𝜑𝐹:𝐴⟶ℂ)
dvtaylp.a (𝜑𝐴𝑆)
dvtaylp.n (𝜑𝑁 ∈ ℕ0)
dvtaylp.b (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)))
Assertion
Ref Expression
dvtaylp (𝜑 → (ℂ D ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵)) = (𝑁(𝑆 Tayl (𝑆 D 𝐹))𝐵))

Proof of Theorem dvtaylp
Dummy variables 𝑗 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2765 . . . . . 6 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
21cnfldtopon 22879 . . . . 5 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
32toponrestid 21019 . . . 4 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
4 cnelprrecn 10286 . . . . 5 ℂ ∈ {ℝ, ℂ}
54a1i 11 . . . 4 (𝜑 → ℂ ∈ {ℝ, ℂ})
6 toponmax 21024 . . . . 5 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
72, 6mp1i 13 . . . 4 (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
8 fzfid 12985 . . . 4 (𝜑 → (0...(𝑁 + 1)) ∈ Fin)
9 dvtaylp.s . . . . . . . . . 10 (𝜑𝑆 ∈ {ℝ, ℂ})
109adantr 472 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → 𝑆 ∈ {ℝ, ℂ})
11 cnex 10274 . . . . . . . . . . . 12 ℂ ∈ V
1211a1i 11 . . . . . . . . . . 11 (𝜑 → ℂ ∈ V)
13 dvtaylp.f . . . . . . . . . . 11 (𝜑𝐹:𝐴⟶ℂ)
14 dvtaylp.a . . . . . . . . . . 11 (𝜑𝐴𝑆)
15 elpm2r 8082 . . . . . . . . . . 11 (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆))
1612, 9, 13, 14, 15syl22anc 867 . . . . . . . . . 10 (𝜑𝐹 ∈ (ℂ ↑pm 𝑆))
1716adantr 472 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → 𝐹 ∈ (ℂ ↑pm 𝑆))
18 elfznn0 12645 . . . . . . . . . 10 (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ0)
1918adantl 473 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℕ0)
20 dvnf 23995 . . . . . . . . 9 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ)
2110, 17, 19, 20syl3anc 1490 . . . . . . . 8 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ)
22 0z 11639 . . . . . . . . . . . 12 0 ∈ ℤ
23 dvtaylp.n . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ0)
24 peano2nn0 11584 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
2523, 24syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ ℕ0)
2625nn0zd 11732 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ ℤ)
27 fzval2 12541 . . . . . . . . . . . 12 ((0 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → (0...(𝑁 + 1)) = ((0[,](𝑁 + 1)) ∩ ℤ))
2822, 26, 27sylancr 581 . . . . . . . . . . 11 (𝜑 → (0...(𝑁 + 1)) = ((0[,](𝑁 + 1)) ∩ ℤ))
2928eleq2d 2830 . . . . . . . . . 10 (𝜑 → (𝑘 ∈ (0...(𝑁 + 1)) ↔ 𝑘 ∈ ((0[,](𝑁 + 1)) ∩ ℤ)))
3029biimpa 468 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ((0[,](𝑁 + 1)) ∩ ℤ))
31 dvtaylp.b . . . . . . . . . 10 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)))
329, 13, 14, 25, 31taylplem1 24422 . . . . . . . . 9 ((𝜑𝑘 ∈ ((0[,](𝑁 + 1)) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))
3330, 32syldan 585 . . . . . . . 8 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))
3421, 33ffvelrnd 6554 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ)
35 faccl 13279 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
3619, 35syl 17 . . . . . . . 8 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (!‘𝑘) ∈ ℕ)
3736nncnd 11296 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (!‘𝑘) ∈ ℂ)
3836nnne0d 11326 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (!‘𝑘) ≠ 0)
3934, 37, 38divcld 11059 . . . . . 6 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ)
40393adant3 1162 . . . . 5 ((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ)
41 simp3 1168 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
42 recnprss 23973 . . . . . . . . . . 11 (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
439, 42syl 17 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℂ)
4414, 43sstrd 3773 . . . . . . . . 9 (𝜑𝐴 ⊆ ℂ)
45 dvnbss 23996 . . . . . . . . . . . 12 ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ (𝑁 + 1) ∈ ℕ0) → dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)) ⊆ dom 𝐹)
469, 16, 25, 45syl3anc 1490 . . . . . . . . . . 11 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)) ⊆ dom 𝐹)
4713, 46fssdmd 6240 . . . . . . . . . 10 (𝜑 → dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)) ⊆ 𝐴)
4847, 31sseldd 3764 . . . . . . . . 9 (𝜑𝐵𝐴)
4944, 48sseldd 3764 . . . . . . . 8 (𝜑𝐵 ∈ ℂ)
50493ad2ant1 1163 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ)
5141, 50subcld 10650 . . . . . 6 ((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → (𝑥𝐵) ∈ ℂ)
52183ad2ant2 1164 . . . . . 6 ((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → 𝑘 ∈ ℕ0)
5351, 52expcld 13220 . . . . 5 ((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → ((𝑥𝐵)↑𝑘) ∈ ℂ)
5440, 53mulcld 10318 . . . 4 ((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥𝐵)↑𝑘)) ∈ ℂ)
55 0cnd 10290 . . . . . 6 (((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ 𝑘 = 0) → 0 ∈ ℂ)
5652nn0cnd 11604 . . . . . . . 8 ((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → 𝑘 ∈ ℂ)
5756adantr 472 . . . . . . 7 (((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℂ)
5851adantr 472 . . . . . . . 8 (((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑥𝐵) ∈ ℂ)
5952adantr 472 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ0)
60 simpr 477 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → ¬ 𝑘 = 0)
6160neqned 2944 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ≠ 0)
62 elnnne0 11558 . . . . . . . . . 10 (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0𝑘 ≠ 0))
6359, 61, 62sylanbrc 578 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ)
64 nnm1nn0 11585 . . . . . . . . 9 (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ0)
6563, 64syl 17 . . . . . . . 8 (((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 − 1) ∈ ℕ0)
6658, 65expcld 13220 . . . . . . 7 (((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → ((𝑥𝐵)↑(𝑘 − 1)) ∈ ℂ)
6757, 66mulcld 10318 . . . . . 6 (((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))) ∈ ℂ)
6855, 67ifclda 4279 . . . . 5 ((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))) ∈ ℂ)
6940, 68mulcld 10318 . . . 4 ((𝜑𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑥 ∈ ℂ) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))) ∈ ℂ)
704a1i 11 . . . . 5 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → ℂ ∈ {ℝ, ℂ})
71533expa 1147 . . . . 5 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → ((𝑥𝐵)↑𝑘) ∈ ℂ)
72683expa 1147 . . . . 5 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))) ∈ ℂ)
73513expa 1147 . . . . . . 7 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → (𝑥𝐵) ∈ ℂ)
74 1cnd 10292 . . . . . . 7 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
75 simpr 477 . . . . . . . 8 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
7619adantr 472 . . . . . . . 8 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑦 ∈ ℂ) → 𝑘 ∈ ℕ0)
7775, 76expcld 13220 . . . . . . 7 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑦 ∈ ℂ) → (𝑦𝑘) ∈ ℂ)
78 c0ex 10291 . . . . . . . . 9 0 ∈ V
79 ovex 6878 . . . . . . . . 9 (𝑘 · (𝑦↑(𝑘 − 1))) ∈ V
8078, 79ifex 4293 . . . . . . . 8 if(𝑘 = 0, 0, (𝑘 · (𝑦↑(𝑘 − 1)))) ∈ V
8180a1i 11 . . . . . . 7 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑦 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · (𝑦↑(𝑘 − 1)))) ∈ V)
82 simpr 477 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
8370dvmptid 24025 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
8449ad2antrr 717 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ)
85 0cnd 10290 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → 0 ∈ ℂ)
8649adantr 472 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → 𝐵 ∈ ℂ)
8770, 86dvmptc 24026 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ 𝐵)) = (𝑥 ∈ ℂ ↦ 0))
8870, 82, 74, 83, 84, 85, 87dvmptsub 24035 . . . . . . . 8 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥𝐵))) = (𝑥 ∈ ℂ ↦ (1 − 0)))
89 1m0e1 11404 . . . . . . . . 9 (1 − 0) = 1
9089mpteq2i 4902 . . . . . . . 8 (𝑥 ∈ ℂ ↦ (1 − 0)) = (𝑥 ∈ ℂ ↦ 1)
9188, 90syl6eq 2815 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥𝐵))) = (𝑥 ∈ ℂ ↦ 1))
92 dvexp2 24022 . . . . . . . 8 (𝑘 ∈ ℕ0 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝑘))) = (𝑦 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · (𝑦↑(𝑘 − 1))))))
9319, 92syl 17 . . . . . . 7 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝑘))) = (𝑦 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · (𝑦↑(𝑘 − 1))))))
94 oveq1 6853 . . . . . . 7 (𝑦 = (𝑥𝐵) → (𝑦𝑘) = ((𝑥𝐵)↑𝑘))
95 oveq1 6853 . . . . . . . . 9 (𝑦 = (𝑥𝐵) → (𝑦↑(𝑘 − 1)) = ((𝑥𝐵)↑(𝑘 − 1)))
9695oveq2d 6862 . . . . . . . 8 (𝑦 = (𝑥𝐵) → (𝑘 · (𝑦↑(𝑘 − 1))) = (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))
9796ifeq2d 4264 . . . . . . 7 (𝑦 = (𝑥𝐵) → if(𝑘 = 0, 0, (𝑘 · (𝑦↑(𝑘 − 1)))) = if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))))
9870, 70, 73, 74, 77, 81, 91, 93, 94, 97dvmptco 24040 . . . . . 6 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ ((𝑥𝐵)↑𝑘))) = (𝑥 ∈ ℂ ↦ (if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))) · 1)))
9972mulid1d 10315 . . . . . . 7 (((𝜑𝑘 ∈ (0...(𝑁 + 1))) ∧ 𝑥 ∈ ℂ) → (if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))) · 1) = if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))))
10099mpteq2dva 4905 . . . . . 6 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (𝑥 ∈ ℂ ↦ (if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))) · 1)) = (𝑥 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))))
10198, 100eqtrd 2799 . . . . 5 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ ((𝑥𝐵)↑𝑘))) = (𝑥 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))))
10270, 71, 72, 101, 39dvmptcmul 24032 . . . 4 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (ℂ D (𝑥 ∈ ℂ ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥𝐵)↑𝑘)))) = (𝑥 ∈ ℂ ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))))))
1033, 1, 5, 7, 8, 54, 69, 102dvmptfsum 24043 . . 3 (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥𝐵)↑𝑘)))) = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))))))
104 1zzd 11660 . . . . . 6 ((𝜑𝑥 ∈ ℂ) → 1 ∈ ℤ)
105 0zd 11640 . . . . . 6 ((𝜑𝑥 ∈ ℂ) → 0 ∈ ℤ)
10623nn0zd 11732 . . . . . . 7 (𝜑𝑁 ∈ ℤ)
107106adantr 472 . . . . . 6 ((𝜑𝑥 ∈ ℂ) → 𝑁 ∈ ℤ)
108 dvfg 23975 . . . . . . . 8 (𝑆 ∈ {ℝ, ℂ} → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)
1099, 108syl 17 . . . . . . 7 (𝜑 → (𝑆 D 𝐹):dom (𝑆 D 𝐹)⟶ℂ)
11043, 13, 14dvbss 23970 . . . . . . . 8 (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝐴)
111110, 14sstrd 3773 . . . . . . 7 (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑆)
112 1nn0 11560 . . . . . . . . . . . 12 1 ∈ ℕ0
113112a1i 11 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℕ0)
114 dvnadd 23997 . . . . . . . . . . 11 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (1 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(1 + 𝑁)))
1159, 16, 113, 23, 114syl22anc 867 . . . . . . . . . 10 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(1 + 𝑁)))
116 dvn1 23994 . . . . . . . . . . . . 13 ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹))
11743, 16, 116syl2anc 579 . . . . . . . . . . . 12 (𝜑 → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹))
118117oveq2d 6862 . . . . . . . . . . 11 (𝜑 → (𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1)) = (𝑆 D𝑛 (𝑆 D 𝐹)))
119118fveq1d 6381 . . . . . . . . . 10 (𝜑 → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘𝑁) = ((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑁))
120 1cnd 10292 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
12123nn0cnd 11604 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
122120, 121addcomd 10496 . . . . . . . . . . 11 (𝜑 → (1 + 𝑁) = (𝑁 + 1))
123122fveq2d 6383 . . . . . . . . . 10 (𝜑 → ((𝑆 D𝑛 𝐹)‘(1 + 𝑁)) = ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)))
124115, 119, 1233eqtr3d 2807 . . . . . . . . 9 (𝜑 → ((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑁) = ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)))
125124dmeqd 5496 . . . . . . . 8 (𝜑 → dom ((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑁) = dom ((𝑆 D𝑛 𝐹)‘(𝑁 + 1)))
12631, 125eleqtrrd 2847 . . . . . . 7 (𝜑𝐵 ∈ dom ((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑁))
1279, 109, 111, 23, 126taylplem2 24423 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ 𝑗 ∈ (0...𝑁)) → (((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥𝐵)↑𝑗)) ∈ ℂ)
128 fveq2 6379 . . . . . . . . 9 (𝑗 = (𝑘 − 1) → ((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗) = ((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1)))
129128fveq1d 6381 . . . . . . . 8 (𝑗 = (𝑘 − 1) → (((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) = (((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵))
130 fveq2 6379 . . . . . . . 8 (𝑗 = (𝑘 − 1) → (!‘𝑗) = (!‘(𝑘 − 1)))
131129, 130oveq12d 6864 . . . . . . 7 (𝑗 = (𝑘 − 1) → ((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) = ((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))))
132 oveq2 6854 . . . . . . 7 (𝑗 = (𝑘 − 1) → ((𝑥𝐵)↑𝑗) = ((𝑥𝐵)↑(𝑘 − 1)))
133131, 132oveq12d 6864 . . . . . 6 (𝑗 = (𝑘 − 1) → (((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥𝐵)↑𝑗)) = (((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥𝐵)↑(𝑘 − 1))))
134104, 105, 107, 127, 133fsumshft 14810 . . . . 5 ((𝜑𝑥 ∈ ℂ) → Σ𝑗 ∈ (0...𝑁)(((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥𝐵)↑𝑗)) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))(((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥𝐵)↑(𝑘 − 1))))
135 elfznn 12582 . . . . . . . . . . . 12 (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ)
136135adantl 473 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈ ℕ)
137136nnne0d 11326 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ≠ 0)
138 ifnefalse 4257 . . . . . . . . . 10 (𝑘 ≠ 0 → if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))) = (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))
139137, 138syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))) = (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))
140139oveq2d 6862 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))))
141 simpll 783 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝜑)
142 fz1ssfz0 12648 . . . . . . . . . . . 12 (1...(𝑁 + 1)) ⊆ (0...(𝑁 + 1))
143142sseli 3759 . . . . . . . . . . 11 (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ (0...(𝑁 + 1)))
144143adantl 473 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈ (0...(𝑁 + 1)))
145141, 144, 39syl2anc 579 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ)
146136nncnd 11296 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑘 ∈ ℂ)
147 simplr 785 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑥 ∈ ℂ)
14849ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐵 ∈ ℂ)
149147, 148subcld 10650 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑥𝐵) ∈ ℂ)
150136, 64syl 17 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑘 − 1) ∈ ℕ0)
151149, 150expcld 13220 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑥𝐵)↑(𝑘 − 1)) ∈ ℂ)
152145, 146, 151mulassd 10321 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 𝑘) · ((𝑥𝐵)↑(𝑘 − 1))) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))))
153 facp1 13274 . . . . . . . . . . . . 13 ((𝑘 − 1) ∈ ℕ0 → (!‘((𝑘 − 1) + 1)) = ((!‘(𝑘 − 1)) · ((𝑘 − 1) + 1)))
154150, 153syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘((𝑘 − 1) + 1)) = ((!‘(𝑘 − 1)) · ((𝑘 − 1) + 1)))
155 1cnd 10292 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 1 ∈ ℂ)
156146, 155npcand 10654 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑘 − 1) + 1) = 𝑘)
157156fveq2d 6383 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘((𝑘 − 1) + 1)) = (!‘𝑘))
158156oveq2d 6862 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((!‘(𝑘 − 1)) · ((𝑘 − 1) + 1)) = ((!‘(𝑘 − 1)) · 𝑘))
159154, 157, 1583eqtr3d 2807 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘𝑘) = ((!‘(𝑘 − 1)) · 𝑘))
160159oveq2d 6862 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / (!‘𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / ((!‘(𝑘 − 1)) · 𝑘)))
16119nn0cnd 11604 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℂ)
16234, 161, 37, 38div23d 11096 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / (!‘𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 𝑘))
163141, 144, 162syl2anc 579 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / (!‘𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 𝑘))
164141, 144, 34syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ)
165 faccl 13279 . . . . . . . . . . . . . 14 ((𝑘 − 1) ∈ ℕ0 → (!‘(𝑘 − 1)) ∈ ℕ)
166150, 165syl 17 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘(𝑘 − 1)) ∈ ℕ)
167166nncnd 11296 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘(𝑘 − 1)) ∈ ℂ)
168166nnne0d 11326 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (!‘(𝑘 − 1)) ≠ 0)
169164, 167, 146, 168, 137divcan5rd 11086 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / ((!‘(𝑘 − 1)) · 𝑘)) = ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘(𝑘 − 1))))
1709ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝑆 ∈ {ℝ, ℂ})
17116ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐹 ∈ (ℂ ↑pm 𝑆))
172112a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 1 ∈ ℕ0)
173 dvnadd 23997 . . . . . . . . . . . . . . 15 (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) ∧ (1 ∈ ℕ0 ∧ (𝑘 − 1) ∈ ℕ0)) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘(𝑘 − 1)) = ((𝑆 D𝑛 𝐹)‘(1 + (𝑘 − 1))))
174170, 171, 172, 150, 173syl22anc 867 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘(𝑘 − 1)) = ((𝑆 D𝑛 𝐹)‘(1 + (𝑘 − 1))))
175117ad2antrr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑆 D𝑛 𝐹)‘1) = (𝑆 D 𝐹))
176175oveq2d 6862 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1)) = (𝑆 D𝑛 (𝑆 D 𝐹)))
177176fveq1d 6381 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑆 D𝑛 ((𝑆 D𝑛 𝐹)‘1))‘(𝑘 − 1)) = ((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1)))
178155, 146pncan3d 10653 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (1 + (𝑘 − 1)) = 𝑘)
179178fveq2d 6383 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑆 D𝑛 𝐹)‘(1 + (𝑘 − 1))) = ((𝑆 D𝑛 𝐹)‘𝑘))
180174, 177, 1793eqtr3rd 2808 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((𝑆 D𝑛 𝐹)‘𝑘) = ((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1)))
181180fveq1d 6381 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) = (((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵))
182181oveq1d 6861 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘(𝑘 − 1))) = ((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))))
183169, 182eqtrd 2799 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) · 𝑘) / ((!‘(𝑘 − 1)) · 𝑘)) = ((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))))
184160, 163, 1833eqtr3d 2807 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 𝑘) = ((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))))
185184oveq1d 6861 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → ((((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 𝑘) · ((𝑥𝐵)↑(𝑘 − 1))) = (((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥𝐵)↑(𝑘 − 1))))
186140, 152, 1853eqtr2d 2805 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))) = (((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥𝐵)↑(𝑘 − 1))))
187186sumeq2dv 14732 . . . . . 6 ((𝜑𝑥 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))) = Σ𝑘 ∈ (1...(𝑁 + 1))(((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥𝐵)↑(𝑘 − 1))))
188 0p1e1 11405 . . . . . . . 8 (0 + 1) = 1
189188oveq1i 6856 . . . . . . 7 ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
190189sumeq1i 14727 . . . . . 6 Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))(((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥𝐵)↑(𝑘 − 1))) = Σ𝑘 ∈ (1...(𝑁 + 1))(((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥𝐵)↑(𝑘 − 1)))
191187, 190syl6eqr 2817 . . . . 5 ((𝜑𝑥 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))(((((𝑆 D𝑛 (𝑆 D 𝐹))‘(𝑘 − 1))‘𝐵) / (!‘(𝑘 − 1))) · ((𝑥𝐵)↑(𝑘 − 1))))
192142a1i 11 . . . . . 6 ((𝜑𝑥 ∈ ℂ) → (1...(𝑁 + 1)) ⊆ (0...(𝑁 + 1)))
19372an32s 642 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 + 1))) → if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))) ∈ ℂ)
194143, 193sylan2 586 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))) ∈ ℂ)
195145, 194mulcld 10318 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (1...(𝑁 + 1))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))) ∈ ℂ)
196 eldif 3744 . . . . . . . . . 10 (𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1))) ↔ (𝑘 ∈ (0...(𝑁 + 1)) ∧ ¬ 𝑘 ∈ (1...(𝑁 + 1))))
19762biimpri 219 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0𝑘 ≠ 0) → 𝑘 ∈ ℕ)
19818, 197sylan 575 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑘 ≠ 0) → 𝑘 ∈ ℕ)
199 nnuz 11928 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
200198, 199syl6eleq 2854 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑘 ≠ 0) → 𝑘 ∈ (ℤ‘1))
201 elfzuz3 12551 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...(𝑁 + 1)) → (𝑁 + 1) ∈ (ℤ𝑘))
202201adantr 472 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑘 ≠ 0) → (𝑁 + 1) ∈ (ℤ𝑘))
203 elfzuzb 12548 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...(𝑁 + 1)) ↔ (𝑘 ∈ (ℤ‘1) ∧ (𝑁 + 1) ∈ (ℤ𝑘)))
204200, 202, 203sylanbrc 578 . . . . . . . . . . . . . 14 ((𝑘 ∈ (0...(𝑁 + 1)) ∧ 𝑘 ≠ 0) → 𝑘 ∈ (1...(𝑁 + 1)))
205204ex 401 . . . . . . . . . . . . 13 (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 ≠ 0 → 𝑘 ∈ (1...(𝑁 + 1))))
206205adantl 473 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑘 ≠ 0 → 𝑘 ∈ (1...(𝑁 + 1))))
207206necon1bd 2955 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (¬ 𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 = 0))
208207impr 446 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ (𝑘 ∈ (0...(𝑁 + 1)) ∧ ¬ 𝑘 ∈ (1...(𝑁 + 1)))) → 𝑘 = 0)
209196, 208sylan2b 587 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → 𝑘 = 0)
210209iftrued 4253 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))) = 0)
211210oveq2d 6862 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0))
212 eldifi 3896 . . . . . . . . 9 (𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1))) → 𝑘 ∈ (0...(𝑁 + 1)))
21339adantlr 706 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ)
214212, 213sylan2 586 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ)
215214mul01d 10493 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0) = 0)
216211, 215eqtrd 2799 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (1...(𝑁 + 1)))) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))) = 0)
217 fzfid 12985 . . . . . 6 ((𝜑𝑥 ∈ ℂ) → (0...(𝑁 + 1)) ∈ Fin)
218192, 195, 216, 217fsumss 14755 . . . . 5 ((𝜑𝑥 ∈ ℂ) → Σ𝑘 ∈ (1...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))) = Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))))
219134, 191, 2183eqtr2rd 2806 . . . 4 ((𝜑𝑥 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1))))) = Σ𝑗 ∈ (0...𝑁)(((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥𝐵)↑𝑗)))
220219mpteq2dva 4905 . . 3 (𝜑 → (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · if(𝑘 = 0, 0, (𝑘 · ((𝑥𝐵)↑(𝑘 − 1)))))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥𝐵)↑𝑗))))
221103, 220eqtrd 2799 . 2 (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥𝐵)↑𝑘)))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥𝐵)↑𝑗))))
222 eqid 2765 . . . 4 ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵) = ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵)
2239, 13, 14, 25, 31, 222taylpfval 24424 . . 3 (𝜑 → ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵) = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥𝐵)↑𝑘))))
224223oveq2d 6862 . 2 (𝜑 → (ℂ D ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 + 1))(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥𝐵)↑𝑘)))))
225 eqid 2765 . . 3 (𝑁(𝑆 Tayl (𝑆 D 𝐹))𝐵) = (𝑁(𝑆 Tayl (𝑆 D 𝐹))𝐵)
2269, 109, 111, 23, 126, 225taylpfval 24424 . 2 (𝜑 → (𝑁(𝑆 Tayl (𝑆 D 𝐹))𝐵) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((((𝑆 D𝑛 (𝑆 D 𝐹))‘𝑗)‘𝐵) / (!‘𝑗)) · ((𝑥𝐵)↑𝑗))))
227221, 224, 2263eqtr4d 2809 1 (𝜑 → (ℂ D ((𝑁 + 1)(𝑆 Tayl 𝐹)𝐵)) = (𝑁(𝑆 Tayl (𝑆 D 𝐹))𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  Vcvv 3350  cdif 3731  cin 3733  wss 3734  ifcif 4245  {cpr 4338  cmpt 4890  dom cdm 5279  wf 6066  cfv 6070  (class class class)co 6846  pm cpm 8065  cc 10191  cr 10192  0cc0 10193  1c1 10194   + caddc 10196   · cmul 10198  cmin 10524   / cdiv 10942  cn 11278  0cn0 11542  cz 11628  cuz 11891  [,]cicc 12385  ...cfz 12538  cexp 13072  !cfa 13269  Σcsu 14715  TopOpenctopn 16362  fldccnfld 20033  TopOnctopon 21008   D cdv 23932   D𝑛 cdvn 23933   Tayl ctayl 24412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-inf2 8757  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271  ax-addf 10272  ax-mulf 10273
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-of 7099  df-om 7268  df-1st 7370  df-2nd 7371  df-supp 7502  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-2o 7769  df-oadd 7772  df-er 7951  df-map 8066  df-pm 8067  df-ixp 8118  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-fsupp 8487  df-fi 8528  df-sup 8559  df-inf 8560  df-oi 8626  df-card 9020  df-cda 9247  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-div 10943  df-nn 11279  df-2 11339  df-3 11340  df-4 11341  df-5 11342  df-6 11343  df-7 11344  df-8 11345  df-9 11346  df-n0 11543  df-z 11629  df-dec 11746  df-uz 11892  df-q 11995  df-rp 12034  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-icc 12389  df-fz 12539  df-fzo 12679  df-seq 13014  df-exp 13073  df-fac 13270  df-hash 13327  df-cj 14138  df-re 14139  df-im 14140  df-sqrt 14274  df-abs 14275  df-clim 14518  df-sum 14716  df-struct 16146  df-ndx 16147  df-slot 16148  df-base 16150  df-sets 16151  df-ress 16152  df-plusg 16241  df-mulr 16242  df-starv 16243  df-sca 16244  df-vsca 16245  df-ip 16246  df-tset 16247  df-ple 16248  df-ds 16250  df-unif 16251  df-hom 16252  df-cco 16253  df-rest 16363  df-topn 16364  df-0g 16382  df-gsum 16383  df-topgen 16384  df-pt 16385  df-prds 16388  df-xrs 16442  df-qtop 16447  df-imas 16448  df-xps 16450  df-mre 16526  df-mrc 16527  df-acs 16529  df-mgm 17522  df-sgrp 17564  df-mnd 17575  df-submnd 17616  df-grp 17706  df-minusg 17707  df-mulg 17822  df-cntz 18027  df-cmn 18475  df-abl 18476  df-mgp 18771  df-ur 18783  df-ring 18830  df-cring 18831  df-psmet 20025  df-xmet 20026  df-met 20027  df-bl 20028  df-mopn 20029  df-fbas 20030  df-fg 20031  df-cnfld 20034  df-top 20992  df-topon 21009  df-topsp 21031  df-bases 21044  df-cld 21117  df-ntr 21118  df-cls 21119  df-nei 21196  df-lp 21234  df-perf 21235  df-cn 21325  df-cnp 21326  df-haus 21413  df-tx 21659  df-hmeo 21852  df-fil 21943  df-fm 22035  df-flim 22036  df-flf 22037  df-tsms 22223  df-xms 22418  df-ms 22419  df-tms 22420  df-cncf 22974  df-limc 23935  df-dv 23936  df-dvn 23937  df-tayl 24414
This theorem is referenced by:  dvntaylp  24430
  Copyright terms: Public domain W3C validator