---

Step * 2 1 1 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
5. d(x^n * x)/dx = λx.(x^n * r1) + (x * r(n) * x^n - 1) on I
6. x : {x:ℝ| x ∈ I} 
⊢ (x^n * x) = x^n + 1
BY
{ (RWO "rnexp-add<" 0 THEN Auto THEN RWO "rpower-one" 0 THEN Auto) }

---

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
5.  d(x\^{}n  *  x)/dx  =  \mlambda{}x.(x\^{}n  *  r1)  +  (x  *  r(n)  *  x\^{}n  -  1)  on  I
6.  x  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
\mvdash{}  (x\^{}n  *  x)  =  x\^{}n  +  1


By

---

Latex:
(RWO  "rnexp-add<"  0  THEN  Auto  THEN  RWO  "rpower-one"  0  THEN  Auto)

---

Home Index