---

Step * 1 1 1 1 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))
11. v : ℝ
12. b : ℝ
13. e^x = b ∈ ℝ
14. a + b^2 = v ∈ ℝ
⊢ ((r(-2) * r(-4) * a * b * b * b)
+ -(r(-4) * r(3) * a * a * b * b)
+ (r(-4) * r(3) * a * b * b * b)
+ (r(-4) * a * a * a * b)
+ -(r(-4) * a * a * b * b))
= ((r(16) * a^2 * b^2) + (r(-4) * a^3 * b) + (r(-4) * b^3 * a))
BY
{ ((RWW  "rmul-assoc rmul-int rminus-as-rmul" 0 THENA Auto) THEN Reduce 0) }

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. b : ℝ
13. e^x = b ∈ ℝ
14. a + b^2 = v ∈ ℝ
⊢ (((((r(8) * a) * b) * b) * b)
+ ((((r(12) * a) * a) * b) * b)
+ ((((r(-12) * a) * b) * b) * b)
+ ((((r(-4) * a) * a) * a) * b)
+ ((((r(4) * a) * a) * b) * b))
= (((r(16) * a^2) * b^2) + ((r(-4) * a^3) * b) + ((r(-4) * b^3) * a))

---

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))
11.  v  :  \mBbbR{}
12.  b  :  \mBbbR{}
13.  e\^{}x  =  b
14.  a  +  b\^{}2  =  v
\mvdash{}  ((r(-2)  *  r(-4)  *  a  *  b  *  b  *  b)
+  -(r(-4)  *  r(3)  *  a  *  a  *  b  *  b)
+  (r(-4)  *  r(3)  *  a  *  b  *  b  *  b)
+  (r(-4)  *  a  *  a  *  a  *  b)
+  -(r(-4)  *  a  *  a  *  b  *  b))
=  ((r(16)  *  a\^{}2  *  b\^{}2)  +  (r(-4)  *  a\^{}3  *  b)  +  (r(-4)  *  b\^{}3  *  a))


By

---

Latex:
((RWW    "rmul-assoc  rmul-int  rminus-as-rmul"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index