---

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


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 ∈ ℝ
7. (a + b^4 + (r(8) * a^3 * b) + (r(8) * b^3 * a))
= ((a^2^2 + b^2^2) + (r(12) * a^3 * b) + (r(12) * b^3 * a) + (r(6) * a^2 * b^2))
8. (r(24) * a * a * b * b) ≤ ((r(12) * a^2 * a * b) + (r(12) * b^2 * a * b))
⊢ (r(24) * a^2 * b^2) ≤ ((r(12) * a^3 * b) + (r(12) * b^3 * a))
BY
{ ((((InstLemma `rnexp_step` [⌜a⌝;⌜3⌝]⋅ THENA Auto) THEN Reduce -1) THEN (RWO "-1" 0 THENA Auto))
   THEN ((InstLemma `rnexp_step` [⌜b⌝;⌜3⌝]⋅ THENA Auto) THEN Reduce -1)
   THEN (RWO "-1" 0 THENA Auto)) }

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 ∈ ℝ
7. (a + b^4 + (r(8) * a^3 * b) + (r(8) * b^3 * a))
= ((a^2^2 + b^2^2) + (r(12) * a^3 * b) + (r(12) * b^3 * a) + (r(6) * a^2 * b^2))
8. (r(24) * a * a * b * b) ≤ ((r(12) * a^2 * a * b) + (r(12) * b^2 * a * b))
9. a^3 = (a^2 * a)
10. b^3 = (b^2 * b)
⊢ (r(24) * a^2 * b^2) ≤ ((r(12) * (a^2 * a) * b) + (r(12) * (b^2 * b) * a))

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  r0  <  a\} 
2.  x  :  \mBbbR{}
3.  \mforall{}x:\mBbbR{}.  (r0  <  (a  +  e\^{}x))
4.  \mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (r0  <  a  +  e\^{}x\^{}n)
5.  b  :  \mBbbR{}
6.  e\^{}x  =  b
7.  (a  +  b\^{}4  +  (r(8)  *  a\^{}3  *  b)  +  (r(8)  *  b\^{}3  *  a))
=  ((a\^{}2\^{}2  +  b\^{}2\^{}2)  +  (r(12)  *  a\^{}3  *  b)  +  (r(12)  *  b\^{}3  *  a)  +  (r(6)  *  a\^{}2  *  b\^{}2))
8.  (r(24)  *  a  *  a  *  b  *  b)  \mleq{}  ((r(12)  *  a\^{}2  *  a  *  b)  +  (r(12)  *  b\^{}2  *  a  *  b))
\mvdash{}  (r(24)  *  a\^{}2  *  b\^{}2)  \mleq{}  ((r(12)  *  a\^{}3  *  b)  +  (r(12)  *  b\^{}3  *  a))


By

---

Latex:
((((InstLemma  `rnexp\_step`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}3\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Reduce  -1)  THEN  (RWO  "-1"  0  THENA  Auto))
  THEN  ((InstLemma  `rnexp\_step`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}3\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Reduce  -1)
  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index