---

Step * 2 1 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
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 * r1) + (x * r(n) * x^n - 1)) = (r(n + 1) * x^(n + 1) - 1)
BY
{ (Subst ⌜(n + 1) - 1 ~ n⌝ 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
6. x : {x:ℝ| x ∈ I} 
⊢ ((x^n * r1) + (x * r(n) * x^n - 1)) = (r(n + 1) * x^n)

---

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  *  r1)  +  (x  *  r(n)  *  x\^{}n  -  1))  =  (r(n  +  1)  *  x\^{}(n  +  1)  -  1)


By

---

Latex:
(Subst  \mkleeneopen{}(n  +  1)  -  1  \msim{}  n\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index