Step
*
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. 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)))
BY
{ Assert ⌜(((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))⌝⋅ }
1
.....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))
2
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. (((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))
⊢ (((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))
11. v : \mBbbR{}
12. a + e\^{}x\^{}2 = v
\mvdash{} (((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)))
By
Latex:
Assert \mkleeneopen{}(((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))\mkleeneclose{}\mcdot{}
Home
Index