---

Step * 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
⊢ d(x^n + 1)/dx = λx.r(n + 1) * x^(n + 1) - 1 on I
BY
{ (DerivativeFunctionality (-1) 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 * x) = x^n + 1

2
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)

---

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


By

---

Latex:
(DerivativeFunctionality  (-1)  THEN  Auto)\mcdot{}

---

Home Index