---

Step * of Lemma polynomial-deriv-seq

∀I:Interval. ∀n:ℕ. ∀a:ℕn + 1 ⟶ ℝ.  finite-deriv-seq(I;n;i,x.rpoly-nth-deriv(i;n;a;x))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN RepUR ``rpoly-nth-deriv`` 0
   THEN RepeatFor 2 (AutoSplit)
   THEN (InstLemma `derivative-rpolynomial` [⌜n - i⌝;⌜poly-nth-deriv(i;a)⌝;⌜I⌝]⋅ THENA Auto)) }

1
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

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}n:\mBbbN{}.  \mforall{}a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}.    finite-deriv-seq(I;n;i,x.rpoly-nth-deriv(i;n;a;x))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``rpoly-nth-deriv``  0
  THEN  RepeatFor  2  (AutoSplit)
  THEN  (InstLemma  `derivative-rpolynomial`  [\mkleeneopen{}n  -  i\mkleeneclose{};\mkleeneopen{}poly-nth-deriv(i;a)\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index