Step
*
of Lemma
derivative-rpolynomial
∀n:ℕ. ∀a:ℕn + 1 ⟶ ℝ. ∀I:Interval. d((Σi≤n. a_i * x^i))/dx = λx.rpoly-deriv(n;a;x) on I
BY
{ (RepUR ``rpoly-deriv poly-deriv`` 0 THEN (InductionOnNat THEN Auto) THEN Reduce 0) }
1
1. a : ℕ0 + 1 ⟶ ℝ
2. I : Interval
⊢ d((Σi≤0. a_i * x^i))/dx = λx.r0 on I
2
1. n : ℤ
2. [%1] : 0 < n
3. ∀a:ℕ(n - 1) + 1 ⟶ ℝ. ∀I:Interval.
d((Σi≤n - 1. a_i * x^i))/dx = λx.if (n - 1 =z 0)
then r0
else (Σi≤n - 1 - 1. λi.(r(i + 1) * (a (i + 1)))_i * x^i)
fi on I
4. a : ℕn + 1 ⟶ ℝ
5. I : Interval
⊢ d((Σi≤n. a_i * x^i))/dx = λx.if (n =z 0) then r0 else (Σi≤n - 1. λi.(r(i + 1) * (a (i + 1)))_i * x^i) fi on I
Latex:
Latex:
\mforall{}n:\mBbbN{}. \mforall{}a:\mBbbN{}n + 1 {}\mrightarrow{} \mBbbR{}. \mforall{}I:Interval. d((\mSigma{}i\mleq{}n. a\_i * x\^{}i))/dx = \mlambda{}x.rpoly-deriv(n;a;x) on I
By
Latex:
(RepUR ``rpoly-deriv poly-deriv`` 0 THEN (InductionOnNat THEN Auto) THEN Reduce 0)
Home
Index