---

Step * of Lemma third-derivative-log-contraction-bound

∀a:{a:ℝ| r0 < a} . ∀x:ℝ.
  ((((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)/a + e^x^4) ≤ (r1/r(2)))
BY
{ (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 nRMul ⌜a + e^x^4⌝ 0⋅
   THEN (GenConcl ⌜e^x = b ∈ ℝ⌝⋅ THENA Auto)
   THEN (nRMul ⌜r(2)⌝ 0⋅ THENA Auto)
   THEN (RWW  "rmul-assoc rmul-int" 0 THENA Auto)
   THEN Reduce 0) }

1
1. a : {a:ℝ| r0 < a} 
2. x : ℝ
3. ∀x:ℝ. (r0 < (a + e^x))
4. ∀x:ℝ. ∀n:ℕ+.  (r0 < a + e^x^n)
5. b : ℝ
6. e^x = b ∈ ℝ
⊢ (((r(32) * a^2) * b^2) + ((r(-8) * a^3) * b) + ((r(-8) * b^3) * a)) ≤ a + b^4

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  r0  <  a\}  .  \mforall{}x:\mBbbR{}.
    ((((r(16)  *  a\^{}2)  *  e\^{}x\^{}2)  +  ((r(-4)  *  a\^{}3)  *  e\^{}x)  +  ((r(-4)  *  a)  *  e\^{}x\^{}3)/a  +  e\^{}x\^{}4)  \mleq{}  (r1/r(2)))


By

---

Latex:
(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  nRMul  \mkleeneopen{}a  +  e\^{}x\^{}4\mkleeneclose{}  0\mcdot{}
  THEN  (GenConcl  \mkleeneopen{}e\^{}x  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (RWW    "rmul-assoc  rmul-int"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index