Step
*
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 * ((((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^2 * (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)))
⊢ (a + e^x^2 * (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3))/a + e^x^4 * a + e^x^2)
= (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)/a + e^x^4)
BY
{ ((Assert (r0 < a + e^x^2) ∧ (r0 < a + e^x^4) BY
Auto)
THEN MoveToConcl (-1)
THEN GenConclTerms Auto [⌜a + e^x^2⌝;⌜a + e^x^4⌝]⋅) }
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 * ((((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^2 * (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)))
11. v : ℝ
12. a + e^x^2 = v ∈ ℝ
13. v1 : ℝ
14. a + e^x^4 = v1 ∈ ℝ
⊢ ((r0 < v) ∧ (r0 < v1))
⇒ ((v * (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3))/v1 * v)
= (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)/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 * ((((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\^{}2 * (((r(16) * a\^{}2) * e\^{}x\^{}2) + ((r(-4) * a\^{}3) * e\^{}x) + ((r(-4) * a) * e\^{}x\^{}3)))
\mvdash{} (a + e\^{}x\^{}2 * (((r(16) * a\^{}2) * e\^{}x\^{}2) + ((r(-4) * a\^{}3) * e\^{}x) + ((r(-4) * a) * e\^{}x\^{}3))/a + e\^{}x\^{}4
* a + e\^{}x\^{}2)
= (((r(16) * a\^{}2) * e\^{}x\^{}2) + ((r(-4) * a\^{}3) * e\^{}x) + ((r(-4) * a) * e\^{}x\^{}3)/a + e\^{}x\^{}4)
By
Latex:
((Assert (r0 < a + e\^{}x\^{}2) \mwedge{} (r0 < a + e\^{}x\^{}4) BY
Auto)
THEN MoveToConcl (-1)
THEN GenConclTerms Auto [\mkleeneopen{}a + e\^{}x\^{}2\mkleeneclose{};\mkleeneopen{}a + e\^{}x\^{}4\mkleeneclose{}]\mcdot{})
Home
Index