---

Step * 1 of Lemma rpoly-nth-deriv-linear


1. d : ℕ
2. n : ℕ
3. ¬d < n
4. a : ℕd + 1 ⟶ ℝ
5. b : ℕd + 1 ⟶ ℝ
6. x : ℝ
⊢ (Σi≤d - n. poly-nth-deriv(n;λi.((a i) + (b i)))_i * x^i)
= ((Σi≤d - n. poly-nth-deriv(n;a)_i * x^i) + (Σi≤d - n. poly-nth-deriv(n;b)_i * x^i))
BY
{ Unfold `rpolynomial` 0 }

1
1. d : ℕ
2. n : ℕ
3. ¬d < n
4. a : ℕd + 1 ⟶ ℝ
5. b : ℕd + 1 ⟶ ℝ
6. x : ℝ
⊢ Σ{(poly-nth-deriv(n;λi.((a i) + (b i))) i) * x^i | 0≤i≤d - n}
= (Σ{(poly-nth-deriv(n;a) i) * x^i | 0≤i≤d - n} + Σ{(poly-nth-deriv(n;b) i) * x^i | 0≤i≤d - n})

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  \mneg{}d  <  n
4.  a  :  \mBbbN{}d  +  1  {}\mrightarrow{}  \mBbbR{}
5.  b  :  \mBbbN{}d  +  1  {}\mrightarrow{}  \mBbbR{}
6.  x  :  \mBbbR{}
\mvdash{}  (\mSigma{}i\mleq{}d  -  n.  poly-nth-deriv(n;\mlambda{}i.((a  i)  +  (b  i)))\_i  *  x\^{}i)
=  ((\mSigma{}i\mleq{}d  -  n.  poly-nth-deriv(n;a)\_i  *  x\^{}i)  +  (\mSigma{}i\mleq{}d  -  n.  poly-nth-deriv(n;b)\_i  *  x\^{}i))


By

---

Latex:
Unfold  `rpolynomial`  0

---

Home Index