---

Step * 1 of Lemma derivative-rnexp


1. n : ℕ+
2. I : Interval
⊢ d(x^1)/dx = λx.r1 * x^1 - 1 on I
BY
{ (Reduce 0 THEN InstLemma `derivative-id` [⌜I⌝]⋅ THEN Auto) }

1
1. n : ℕ+
2. I : Interval
3. d(x)/dx = λx.r1 on I
⊢ d(x^1)/dx = λx.r1 * r1 on I

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  I  :  Interval
\mvdash{}  d(x\^{}1)/dx  =  \mlambda{}x.r1  *  x\^{}1  -  1  on  I


By

---

Latex:
(Reduce  0  THEN  InstLemma  `derivative-id`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index