Step
*
1
1
1
1
1
2
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. (((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)))
BY
{ (MoveToConcl (-1)
THEN GenConclTerms Auto [⌜((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)⌝]⋅
THEN GenConclTerms Auto [⌜a + e^x⌝;⌜r0 - e^x⌝;⌜r0 + e^x⌝;⌜a - e^x⌝]⋅) }
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. 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))
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. (((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))
\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:
(MoveToConcl (-1)
THEN GenConclTerms Auto [\mkleeneopen{}((r(16) * a\^{}2) * e\^{}x\^{}2) + ((r(-4) * a\^{}3) * e\^{}x) + ((r(-4) * a) * e\^{}x\^{}3)\mkleeneclose{}]
\mcdot{}
THEN GenConclTerms Auto [\mkleeneopen{}a + e\^{}x\mkleeneclose{};\mkleeneopen{}r0 - e\^{}x\mkleeneclose{};\mkleeneopen{}r0 + e\^{}x\mkleeneclose{};\mkleeneopen{}a - e\^{}x\mkleeneclose{}]\mcdot{})
Home
Index