---

Step * of Lemma derivative-rinv-basic

d((r1/x))/dx = λx.(r(-1)/x^2) on (r0, ∞)
BY
{ (InstLemma `derivative-rinv` [⌜(r0, ∞)⌝;⌜λ2x.x⌝;⌜λ2x.r1⌝]⋅ THENA Auto) }

1
.....antecedent..... 
x≠r0 for x ∈ (r0, ∞)

2
1. d((r1/x))/dx = λx.(-(r1)/x * x) on (r0, ∞)
⊢ d((r1/x))/dx = λx.(r(-1)/x^2) on (r0, ∞)

---

Latex:

---

Latex:
d((r1/x))/dx  =  \mlambda{}x.(r(-1)/x\^{}2)  on  (r0,  \minfty{})


By

---

Latex:
(InstLemma  `derivative-rinv`  [\mkleeneopen{}(r0,  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.r1\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index