---

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


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 ∈ (-∞, ∞)} 
9. (a + e^x^3 * a + e^x^3) = (a + e^x^4 * a + e^x^2)
10. a + e^x^3 = (a + e^x^2 * (a + e^x))
⊢ (((a + e^x^2 * (a + e^x)) * ((((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^2 * (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)))
BY
{ (GenConclTerm ⌜a + e^x^2⌝⋅ THENA 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 ∈ (-∞, ∞)} 
9. (a + e^x^3 * a + e^x^3) = (a + e^x^4 * a + e^x^2)
10. a + e^x^3 = (a + e^x^2 * (a + e^x))
11. v : ℝ
12. a + e^x^2 = v ∈ ℝ
⊢ (((v * (a + e^x)) * ((((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) * v)
* (r0 + e^x))
= (v * (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)))

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  r0  <  a\} 
2.  r0  <  a
3.  a  +  e\^{}x\^{}3\mneq{}r0  for  x  \mmember{}  (-\minfty{},  \minfty{})
4.  \mforall{}x:\mBbbR{}.  (r0  <  (a  +  e\^{}x))
5.  \mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (r0  <  a  +  e\^{}x\^{}n)
6.  \mforall{}x:\mBbbR{}.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (r0  <  (a  +  e\^{}x\^{}n  *  a  +  e\^{}x\^{}m))
7.  d((((r(-4)  *  a)  *  e\^{}x)  *  (a  -  e\^{}x)/a  +  e\^{}x\^{}3))/dx  =  \mlambda{}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  (-\minfty{},  \minfty{})
8.  x  :  \{x:\mBbbR{}|  x  \mmember{}  (-\minfty{},  \minfty{})\} 
9.  (a  +  e\^{}x\^{}3  *  a  +  e\^{}x\^{}3)  =  (a  +  e\^{}x\^{}4  *  a  +  e\^{}x\^{}2)
10.  a  +  e\^{}x\^{}3  =  (a  +  e\^{}x\^{}2  *  (a  +  e\^{}x))
\mvdash{}  (((a  +  e\^{}x\^{}2  *  (a  +  e\^{}x))
*  ((((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\^{}2  *  (((r(16)  *  a\^{}2)  *  e\^{}x\^{}2)  +  ((r(-4)  *  a\^{}3)  *  e\^{}x)  +  ((r(-4)  *  a)  *  e\^{}x\^{}3)))


By

---

Latex:
(GenConclTerm  \mkleeneopen{}a  +  e\^{}x\^{}2\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index