---

Step * 1 1 1 1 2 of Lemma rexp-rlog


1. x : ℝ
2. r0 < x
3. e^rlog(x) ≠ x
4. d(rlog(x))/dx = λx.(r1/x) on (r0, ∞)
5. x_∫-e^rlog(x) (r1/t) dt = (rlog(e^rlog(x)) - rlog(x))
⊢ x_∫-e^rlog(x) (r1/t) dt = r0
BY
{ (RWO "-1" 0
   THEN Auto
   THEN Try ((RWO  "-1" 0 THEN Auto))
   THEN Try ((OrRight
              THEN Auto
              THEN DSetVars
              THEN Unhide
              THEN Auto
              THEN All Reduce
              THEN ExRepD
              THEN (RWO "-2< -3< 7<" 0 THENA Auto)
              THEN EAuto 1
              THEN BLemma `rmin_strict_ub`
              THEN Auto))) }

1
1. x : ℝ
2. r0 < x
3. e^rlog(x) ≠ x
4. d(rlog(x))/dx = λx.(r1/x) on (r0, ∞)
5. x_∫-e^rlog(x) (r1/t) dt = (rlog(e^rlog(x)) - rlog(x))
⊢ (rlog(e^rlog(x)) - rlog(x)) = r0

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  r0  <  x
3.  e\^{}rlog(x)  \mneq{}  x
4.  d(rlog(x))/dx  =  \mlambda{}x.(r1/x)  on  (r0,  \minfty{})
5.  x\_\mint{}\msupminus{}e\^{}rlog(x)  (r1/t)  dt  =  (rlog(e\^{}rlog(x))  -  rlog(x))
\mvdash{}  x\_\mint{}\msupminus{}e\^{}rlog(x)  (r1/t)  dt  =  r0


By

---

Latex:
(RWO  "-1"  0
  THEN  Auto
  THEN  Try  ((RWO    "-1"  0  THEN  Auto))
  THEN  Try  ((OrRight
                        THEN  Auto
                        THEN  DSetVars
                        THEN  Unhide
                        THEN  Auto
                        THEN  All  Reduce
                        THEN  ExRepD
                        THEN  (RWO  "-2<  -3<  7<"  0  THENA  Auto)
                        THEN  EAuto  1
                        THEN  BLemma  `rmin\_strict\_ub`
                        THEN  Auto)))

---

Home Index