---

Step * 1 1 of Lemma polynomial-deriv-seq


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)
BY
{ (EqCD THEN Auto) }

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
⊢ poly-nth-deriv(i + 1;a) ~ poly-deriv(poly-nth-deriv(i;a))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  n  :  \mBbbN{}
3.  a  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
4.  i  :  \mBbbN{}n
5.  n  -  i  \mneq{}  0
6.  \mneg{}n  <  i  +  1
7.  \mneg{}n  <  i
8.  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
9.  x  :  Base
\mvdash{}  (\mSigma{}i\mleq{}n  -  i  +  1.  poly-nth-deriv(i  +  1;a)\_i  *  x\^{}i)  \msim{}  (\mSigma{}i\mleq{}n  -  i 
-  1.  poly-deriv(poly-nth-deriv(i;a))\_i  *  x\^{}i)


By

---

Latex:
(EqCD  THEN  Auto)

---

Home Index