---

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

∀a:{a:ℝ| r0 < a} . ∀x:ℝ.
  ((|x - rlog(a)| ≤ r1) ⇒ (r0 ≤ (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)/a + e^x^4)))
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⋅) }

1
1. a : {a:ℝ| r0 < a} 
2. x : ℝ
3. |x - rlog(a)| ≤ r1
4. ∀x:ℝ. (r0 < (a + e^x))
5. ∀x:ℝ. ∀n:ℕ+.  (r0 < a + e^x^n)
⊢ r0 ≤ ((r(-4) * e^x * a^3) + (r(16) * e^x^2 * a^2) + (r(-4) * e^x^3 * a))

---

Latex:

---

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


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{})

---

Home Index