---

Step * 1 of Lemma polynomial-deriv-seq


1. I : Interval
2. n : ℕ
3. a : ℕn + 1 ⟶ ℝ
4. i : ℕn
5. ¬n < i + 1
6. ¬n < i
7. d((Σi≤n - i. poly-nth-deriv(i;a)_i * x^i))/dx = λx.rpoly-deriv(n - i;poly-nth-deriv(i;a);x) on I
⊢ d((Σi≤n - i. poly-nth-deriv(i;a)_i * x^i))/dx = λx.(Σi≤n - i + 1. poly-nth-deriv(i + 1;a)_i * x^i) on I
BY
{ (NthHypSq (-1) THEN EqCD THEN Auto THEN RepUR ``rpoly-deriv`` 0 THEN AutoSplit) }

1
1. I : Interval
2. n : ℕ
3. a : ℕn + 1 ⟶ ℝ
4. i : ℕn
5. n - i ≠ 0
6. ¬n < i + 1
7. ¬n < i
8. d((Σi≤n - i. poly-nth-deriv(i;a)_i * x^i))/dx = λx.rpoly-deriv(n - i;poly-nth-deriv(i;a);x) on I
9. x : Base
⊢ (Σi≤n - i + 1. poly-nth-deriv(i + 1;a)_i * x^i) ~ (Σi≤n - i - 1. poly-deriv(poly-nth-deriv(i;a))_i * x^i)

---

Latex:

---

Latex:

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


By

---

Latex:
(NthHypSq  (-1)  THEN  EqCD  THEN  Auto  THEN  RepUR  ``rpoly-deriv``  0  THEN  AutoSplit)

---

Home Index