---

Step * of Lemma derivative-rsqrt

d(rsqrt(x))/dx = λx.(r1/r(2) * rsqrt(x)) on (r0, ∞)
BY
{ (InstLemma `derivative-rexp-function`
    [⌜(r0, ∞)⌝;⌜λ2x.(r1/r(2)) * rlog(x)⌝;⌜λ2x.(r1/r(2)) * (r1/x)⌝]⋅
   THENA (Auto THEN Try ((RWO "-1" 0 THEN Auto)) THEN ProveDerivative THEN Auto)
   ) }

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

---

Latex:

---

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


By

---

Latex:
(InstLemma  `derivative-rexp-function`
    [\mkleeneopen{}(r0,  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(r1/r(2))  *  rlog(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(r1/r(2))  *  (r1/x)\mkleeneclose{}]\mcdot{}
  THENA  (Auto  THEN  Try  ((RWO  "-1"  0  THEN  Auto))  THEN  ProveDerivative  THEN  Auto)
  )

---

Home Index