---

Step * of Lemma third-derivative-log-contraction

∀a:{a:ℝ| r0 < a} 
  d((((r(-4) * a) * e^x) * (a - e^x)/a + e^x^3))/dx = λx.(((r(16) * a^2) * e^x^2)
  + ((r(-4) * a^3) * e^x)
  + ((r(-4) * a) * e^x^3)/a + e^x^4) on (-∞, ∞)
BY
{ ((Auto
    THEN (Assert r0 < a BY
                Auto)
    THEN (Assert a + e^x^3≠r0 for x ∈ (-∞, ∞) BY
                ((D 0 THENA Auto)
                 THEN D 0 With ⌜a^3⌝ 
                 THEN (Auto THEN Try ((BLemma `rnexp-positive` THEN Auto)))
                 THEN (RWO "rabs-of-nonneg" 0 THEN Auto)
                 THEN Try ((BLemma `rnexp-nonneg` THEN Auto))
                 THEN Try ((BLemma `rnexp-rleq` THEN Auto))
                 THEN (RWW "rexp-positive<" 0 THENM nRNorm 0)
                 THEN Auto)))
   THEN (Assert ∀x:ℝ. (r0 < (a + e^x)) BY
               (Auto THEN (RWW "rexp-positive<" 0 THENM nRNorm 0) THEN Auto))
   THEN (Assert ∀x:ℝ. ∀n:ℕ+.  (r0 < a + e^x^n) BY
               (Auto THEN BLemma `rnexp-positive` THEN Auto))
   THEN (Assert ∀x:ℝ. ∀n,m:ℕ+.  (r0 < (a + e^x^n * a + e^x^m)) BY
               (Auto THEN BLemma `rmul-is-positive` THEN Auto))
   THEN (AssertDerivative THENA (ProveDerivative THEN Auto))
   THEN DerivativeFunctionality (-1)
   THEN Auto) }

1
1. a : {a:ℝ| r0 < a} 
2. r0 < a
3. a + e^x^3≠r0 for x ∈ (-∞, ∞)
4. ∀x:ℝ. (r0 < (a + e^x))
5. ∀x:ℝ. ∀n:ℕ+.  (r0 < a + e^x^n)
6. ∀x:ℝ. ∀n,m:ℕ+.  (r0 < (a + e^x^n * a + e^x^m))
7. d((((r(-4) * a) * e^x) * (a - e^x)/a + e^x^3))/dx = λx.((a + e^x^3
* ((((r(-4) * a) * e^x) * (r0 - e^x)) + ((a - e^x) * (r(-4) * a) * e^x))) - (((r(-4) * a) * e^x) * (a - e^x))
* (r(3) * a + e^x^2)
* (r0 + e^x)/a + e^x^3 * a + e^x^3) on (-∞, ∞)
8. x : {x:ℝ| x ∈ (-∞, ∞)} 
⊢ ((a + e^x^3 * ((((r(-4) * a) * e^x) * (r0 - e^x)) + ((a - e^x) * (r(-4) * a) * e^x))) - (((r(-4) * a) * e^x)
                                                                                          * (a - e^x))
* (r(3) * a + e^x^2)
* (r0 + e^x)/a + e^x^3 * a + e^x^3)
= (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)/a + e^x^4)

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  r0  <  a\} 
    d((((r(-4)  *  a)  *  e\^{}x)  *  (a  -  e\^{}x)/a  +  e\^{}x\^{}3))/dx  =  \mlambda{}x.(((r(16)  *  a\^{}2)  *  e\^{}x\^{}2)
    +  ((r(-4)  *  a\^{}3)  *  e\^{}x)
    +  ((r(-4)  *  a)  *  e\^{}x\^{}3)/a  +  e\^{}x\^{}4)  on  (-\minfty{},  \minfty{})


By

---

Latex:
((Auto
    THEN  (Assert  r0  <  a  BY
                            Auto)
    THEN  (Assert  a  +  e\^{}x\^{}3\mneq{}r0  for  x  \mmember{}  (-\minfty{},  \minfty{})  BY
                            ((D  0  THENA  Auto)
                              THEN  D  0  With  \mkleeneopen{}a\^{}3\mkleeneclose{} 
                              THEN  (Auto  THEN  Try  ((BLemma  `rnexp-positive`  THEN  Auto)))
                              THEN  (RWO  "rabs-of-nonneg"  0  THEN  Auto)
                              THEN  Try  ((BLemma  `rnexp-nonneg`  THEN  Auto))
                              THEN  Try  ((BLemma  `rnexp-rleq`  THEN  Auto))
                              THEN  (RWW  "rexp-positive<"  0  THENM  nRNorm  0)
                              THEN  Auto)))
  THEN  (Assert  \mforall{}x:\mBbbR{}.  (r0  <  (a  +  e\^{}x))  BY
                          (Auto  THEN  (RWW  "rexp-positive<"  0  THENM  nRNorm  0)  THEN  Auto))
  THEN  (Assert  \mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (r0  <  a  +  e\^{}x\^{}n)  BY
                          (Auto  THEN  BLemma  `rnexp-positive`  THEN  Auto))
  THEN  (Assert  \mforall{}x:\mBbbR{}.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (r0  <  (a  +  e\^{}x\^{}n  *  a  +  e\^{}x\^{}m))  BY
                          (Auto  THEN  BLemma  `rmul-is-positive`  THEN  Auto))
  THEN  (AssertDerivative  THENA  (ProveDerivative  THEN  Auto))
  THEN  DerivativeFunctionality  (-1)
  THEN  Auto)

---

Home Index