---

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

.....assertion..... 
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 ∈ ℝ
⊢ (((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)
* (r0 + e^x))
= (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3))
BY
{ ((Unfold `rsub` 0 THEN (RWO "radd-zero-both.2" 0 THENA Auto))
   THEN MoveToConcl (-1)
   THEN GenConcl ⌜e^x = b ∈ ℝ⌝⋅
   THEN Auto
   THEN (RWO  "rminus-as-rmul" 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)
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 ∈ ℝ
⊢ (((a + b) * ((((r(-4) * a) * b) * r(-1) * b) + ((a + (r(-1) * b)) * (r(-4) * a) * b)))
+ (r(-1) * (((r(-4) * a) * b) * (a + -(b))) * r(3) * b))
= (((r(16) * a^2) * b^2) + ((r(-4) * a^3) * b) + ((r(-4) * a) * b^3))

---

Latex:

---

Latex:
.....assertion..... 
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.  a  +  e\^{}x\^{}2  =  v
\mvdash{}  (((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)
*  (r0  +  e\^{}x))
=  (((r(16)  *  a\^{}2)  *  e\^{}x\^{}2)  +  ((r(-4)  *  a\^{}3)  *  e\^{}x)  +  ((r(-4)  *  a)  *  e\^{}x\^{}3))


By

---

Latex:
((Unfold  `rsub`  0  THEN  (RWO  "radd-zero-both.2"  0  THENA  Auto))
  THEN  MoveToConcl  (-1)
  THEN  GenConcl  \mkleeneopen{}e\^{}x  =  b\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (RWO    "rminus-as-rmul"  0  THENA  Auto))

---

Home Index