---

Step * of Lemma poly-nth-deriv-req

∀[n,d:ℕ]. ∀[a:ℕn + d ⟶ ℝ]. ∀[i:ℕd].  ((poly-nth-deriv(n;a) i) = (r((i + n)!) * (a (i + n)))/(i)!)
BY
{ (InductionOnNat THEN Auto) }

1
1. n : ℤ
2. d : ℕ
3. a : ℕ0 + d ⟶ ℝ
4. i : ℕd
⊢ (poly-nth-deriv(0;a) i) = (r((i + 0)!) * (a (i + 0)))/(i)!

2
1. n : ℤ
2. 0 < n
3. ∀[d:ℕ]. ∀[a:ℕ(n - 1) + d ⟶ ℝ]. ∀[i:ℕd].
     ((poly-nth-deriv(n - 1;a) i) = (r((i + (n - 1))!) * (a (i + (n - 1))))/(i)!)
4. d : ℕ
5. a : ℕn + d ⟶ ℝ
6. i : ℕd
⊢ (poly-nth-deriv(n;a) i) = (r((i + n)!) * (a (i + n)))/(i)!

---

Latex:

---

Latex:
\mforall{}[n,d:\mBbbN{}].  \mforall{}[a:\mBbbN{}n  +  d  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[i:\mBbbN{}d].    ((poly-nth-deriv(n;a)  i)  =  (r((i  +  n)!)  *  (a  (i  +  n)))/(i)!)


By

---

Latex:
(InductionOnNat  THEN  Auto)

---

Home Index