---

Step * 1 1 1 1 1 2 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. a + e^x^2 = v ∈ ℝ
13. v1 : ℝ
14. (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)) = v1 ∈ ℝ
15. v2 : ℝ
16. (a + e^x) = v2 ∈ ℝ
17. v3 : ℝ
18. (r0 - e^x) = v3 ∈ ℝ
19. v4 : ℝ
20. (r0 + e^x) = v4 ∈ ℝ
21. v5 : ℝ
22. (a - e^x) = v5 ∈ ℝ
⊢ (((v2 * ((((r(-4) * a) * e^x) * v3) + (v5 * (r(-4) * a) * e^x))) - (((r(-4) * a) * e^x) * v5) * r(3) * v4) = v1)
⇒ ((((v * v2) * ((((r(-4) * a) * e^x) * v3) + (v5 * (r(-4) * a) * e^x))) - (((r(-4) * a) * e^x) * v5)
   * (r(3) * v)
   * v4)
   = (v * v1))
BY
{ ((D 0 THENA Auto) THEN (nRMul ⌜v⌝ (-1)⋅ THENA Auto) THEN nRNorm 0 THEN Auto) }

---

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.  a  +  e\^{}x\^{}2  =  v
13.  v1  :  \mBbbR{}
14.  (((r(16)  *  a\^{}2)  *  e\^{}x\^{}2)  +  ((r(-4)  *  a\^{}3)  *  e\^{}x)  +  ((r(-4)  *  a)  *  e\^{}x\^{}3))  =  v1
15.  v2  :  \mBbbR{}
16.  (a  +  e\^{}x)  =  v2
17.  v3  :  \mBbbR{}
18.  (r0  -  e\^{}x)  =  v3
19.  v4  :  \mBbbR{}
20.  (r0  +  e\^{}x)  =  v4
21.  v5  :  \mBbbR{}
22.  (a  -  e\^{}x)  =  v5
\mvdash{}  (((v2  *  ((((r(-4)  *  a)  *  e\^{}x)  *  v3)  +  (v5  *  (r(-4)  *  a)  *  e\^{}x)))  -  (((r(-4)  *  a)  *  e\^{}x)  *  v5)
*  r(3)
*  v4)
=  v1)
{}\mRightarrow{}  ((((v  *  v2)  *  ((((r(-4)  *  a)  *  e\^{}x)  *  v3)  +  (v5  *  (r(-4)  *  a)  *  e\^{}x)))  -  (((r(-4)  *  a)  *  e\^{}x)
                                                                                                                                                        *  v5)
      *  (r(3)  *  v)
      *  v4)
      =  (v  *  v1))


By

---

Latex:
((D  0  THENA  Auto)  THEN  (nRMul  \mkleeneopen{}v\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)  THEN  nRNorm  0  THEN  Auto)

---

Home Index