---

Step * 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 ∈ (-∞, ∞)} 
⊢ ((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)
BY
{ ((Assert (a + e^x^3 * a + e^x^3) = (a + e^x^4 * a + e^x^2) BY
          ((RWO "rnexp-add" 0 THENM Reduce 0) THEN Auto))
   THEN (RWO  "-1" 0 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)
⊢ ((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^4 * a + e^x^2)
= (((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:

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{})\} 
\mvdash{}  ((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)


By

---

Latex:
((Assert  (a  +  e\^{}x\^{}3  *  a  +  e\^{}x\^{}3)  =  (a  +  e\^{}x\^{}4  *  a  +  e\^{}x\^{}2)  BY
                ((RWO  "rnexp-add"  0  THENM  Reduce  0)  THEN  Auto))
  THEN  (RWO    "-1"  0  THENA  Auto)
  )

---

Home Index