---

Step * 2 of Lemma derivative-rnexp


1. n : ℤ
2. 0 < n
3. ∀I:Interval. d(x^n)/dx = λx.r(n) * x^n - 1 on I
4. I : Interval
⊢ d(x^n + 1)/dx = λx.r(n + 1) * x^(n + 1) - 1 on I
BY
{ (InstLemma `derivative-mul` [⌜I⌝;⌜λ2x.x^n⌝;⌜λ2x.x⌝;⌜λ2x.r(n) * x^n - 1⌝;⌜λ2x.r1⌝]⋅
   THENA (Auto THEN RepUR ``so_lambda r-ap`` 0 THEN Try (Complete ((MemTypeCD THEN Reduce 0 THEN Auto))))
   ) }

1
1. n : ℤ
2. 0 < n
3. ∀I:Interval. d(x^n)/dx = λx.r(n) * x^n - 1 on I
4. I : Interval
5. d(x^n * x)/dx = λx.(x^n * r1) + (x * r(n) * x^n - 1) on I
⊢ d(x^n + 1)/dx = λx.r(n + 1) * x^(n + 1) - 1 on I

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}I:Interval.  d(x\^{}n)/dx  =  \mlambda{}x.r(n)  *  x\^{}n  -  1  on  I
4.  I  :  Interval
\mvdash{}  d(x\^{}n  +  1)/dx  =  \mlambda{}x.r(n  +  1)  *  x\^{}(n  +  1)  -  1  on  I


By

---

Latex:
(InstLemma  `derivative-mul`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\^{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.r(n)  *  x\^{}n  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.r1\mkleeneclose{}]\mcdot{}
  THENA  (Auto
                THEN  RepUR  ``so\_lambda  r-ap``  0
                THEN  Try  (Complete  ((MemTypeCD  THEN  Reduce  0  THEN  Auto))))
  )

---

Home Index