---

Step * 2 1 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} 
7. (x * r(n) * x^n - 1) = (r(n) * x^(n - 1) + 1)
⊢ ((x^n * r1) + (r(n) * x^n)) = (r(n + 1) * x^n)
BY
{ ((RWO "radd-int<" 0 THEN Auto) THEN GenConclTerm ⌜r(n)⌝⋅ 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\} 
7.  (x  *  r(n)  *  x\^{}n  -  1)  =  (r(n)  *  x\^{}(n  -  1)  +  1)
\mvdash{}  ((x\^{}n  *  r1)  +  (r(n)  *  x\^{}n))  =  (r(n  +  1)  *  x\^{}n)


By

---

Latex:
((RWO  "radd-int<"  0  THEN  Auto)  THEN  GenConclTerm  \mkleeneopen{}r(n)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index