---

Step * 2 1 2 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 * r1) + (x * r(n) * x^n - 1)) = (r(n + 1) * x^n)
BY
{ ((Assert (x * r(n) * x^n - 1) = (r(n) * x^(n - 1) + 1) BY
          ((RWW "rnexp-add< rpower-one" 0 THENM nRNorm 0) THEN Auto))
   THEN ((RWO "-1" 0 THENA Auto) THEN Subst ⌜(n - 1) + 1 ~ n⌝ 0⋅ THEN Auto)
   THEN skip{(nRNorm 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} 
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)

---

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)


By

---

Latex:
((Assert  (x  *  r(n)  *  x\^{}n  -  1)  =  (r(n)  *  x\^{}(n  -  1)  +  1)  BY
                ((RWW  "rnexp-add<  rpower-one"  0  THENM  nRNorm  0)  THEN  Auto))
  THEN  ((RWO  "-1"  0  THENA  Auto)  THEN  Subst  \mkleeneopen{}(n  -  1)  +  1  \msim{}  n\mkleeneclose{}  0\mcdot{}  THEN  Auto)
  THEN  skip\{(nRNorm  0  THEN  Auto)\})

---

Home Index