---

Step * of Lemma rpoly-nth-deriv-linear

∀[d,n:ℕ]. ∀[a,b:ℕd + 1 ⟶ ℝ]. ∀[x:ℝ].
  (rpoly-nth-deriv(n;d;λi.((a i) + (b i));x) = (rpoly-nth-deriv(n;d;a;x) + rpoly-nth-deriv(n;d;b;x)))
BY
{ (Auto THEN RepUR ``rpoly-nth-deriv`` 0 THEN AutoSplit) }

1
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))

---

Latex:

---

Latex:
\mforall{}[d,n:\mBbbN{}].  \mforall{}[a,b:\mBbbN{}d  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x:\mBbbR{}].
    (rpoly-nth-deriv(n;d;\mlambda{}i.((a  i)  +  (b  i));x)
    =  (rpoly-nth-deriv(n;d;a;x)  +  rpoly-nth-deriv(n;d;b;x)))


By

---

Latex:
(Auto  THEN  RepUR  ``rpoly-nth-deriv``  0  THEN  AutoSplit)

---

Home Index