Step
*
2
1
1
2
2
1
1
of Lemma
small-arcsine
1. N : ℕ+
2. a : ℝ
3. |a| ≤ (r1/r(N + 1))
4. a ∈ (r(-1), r1)
5. ∀f,f':[-((r1/r(N + 1))), (r1/r(N + 1))] ⟶ℝ.
((∀x,y:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . ((x = y) ⇒ (f'[x] = f'[y])))
⇒ d(f[x])/dx = λx.f'[x] on [-((r1/r(N + 1))), (r1/r(N + 1))]
⇒ (∀c:ℝ
((∀x:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|f'[x]| ≤ c))
⇒ (∀x,y:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|f[x] - f[y]| ≤ (c * |x - y|))))))
6. [-((r1/r(N + 1))), (r1/r(N + 1))] ⊆ (r(-1), r1)
7. ∀c:ℝ
((∀x:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|arcsine_deriv(x)| ≤ c))
⇒ (∀x,y:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|arcsine(x) - arcsine(y)| ≤ (c * |x - y|))))
8. 0 < N * (N + 1)
9. r0 < r(N * (N + 1))
10. r0 < rsqrt(r(N * (N + 1)))
11. x : {x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]}
⊢ |arcsine_deriv(x)| ≤ (r(N + 1)/rsqrt(r(N * (N + 1))))
BY
{ (InstLemma `rnexp-rleq` [⌜|x|⌝;⌜(r1/r(N + 1))⌝;⌜2⌝]⋅ THENA Auto) }
1
.....antecedent.....
1. N : ℕ+
2. a : ℝ
3. |a| ≤ (r1/r(N + 1))
4. a ∈ (r(-1), r1)
5. ∀f,f':[-((r1/r(N + 1))), (r1/r(N + 1))] ⟶ℝ.
((∀x,y:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . ((x = y) ⇒ (f'[x] = f'[y])))
⇒ d(f[x])/dx = λx.f'[x] on [-((r1/r(N + 1))), (r1/r(N + 1))]
⇒ (∀c:ℝ
((∀x:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|f'[x]| ≤ c))
⇒ (∀x,y:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|f[x] - f[y]| ≤ (c * |x - y|))))))
6. [-((r1/r(N + 1))), (r1/r(N + 1))] ⊆ (r(-1), r1)
7. ∀c:ℝ
((∀x:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|arcsine_deriv(x)| ≤ c))
⇒ (∀x,y:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|arcsine(x) - arcsine(y)| ≤ (c * |x - y|))))
8. 0 < N * (N + 1)
9. r0 < r(N * (N + 1))
10. r0 < rsqrt(r(N * (N + 1)))
11. x : {x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]}
⊢ |x| ≤ (r1/r(N + 1))
2
1. N : ℕ+
2. a : ℝ
3. |a| ≤ (r1/r(N + 1))
4. a ∈ (r(-1), r1)
5. ∀f,f':[-((r1/r(N + 1))), (r1/r(N + 1))] ⟶ℝ.
((∀x,y:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . ((x = y) ⇒ (f'[x] = f'[y])))
⇒ d(f[x])/dx = λx.f'[x] on [-((r1/r(N + 1))), (r1/r(N + 1))]
⇒ (∀c:ℝ
((∀x:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|f'[x]| ≤ c))
⇒ (∀x,y:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|f[x] - f[y]| ≤ (c * |x - y|))))))
6. [-((r1/r(N + 1))), (r1/r(N + 1))] ⊆ (r(-1), r1)
7. ∀c:ℝ
((∀x:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|arcsine_deriv(x)| ≤ c))
⇒ (∀x,y:{x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]} . (|arcsine(x) - arcsine(y)| ≤ (c * |x - y|))))
8. 0 < N * (N + 1)
9. r0 < r(N * (N + 1))
10. r0 < rsqrt(r(N * (N + 1)))
11. x : {x:ℝ| x ∈ [-((r1/r(N + 1))), (r1/r(N + 1))]}
12. |x|^2 ≤ (r1/r(N + 1))^2
⊢ |arcsine_deriv(x)| ≤ (r(N + 1)/rsqrt(r(N * (N + 1))))
Latex:
Latex:
1. N : \mBbbN{}\msupplus{}
2. a : \mBbbR{}
3. |a| \mleq{} (r1/r(N + 1))
4. a \mmember{} (r(-1), r1)
5. \mforall{}f,f':[-((r1/r(N + 1))), (r1/r(N + 1))] {}\mrightarrow{}\mBbbR{}.
((\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [-((r1/r(N + 1))), (r1/r(N + 1))]\} . ((x = y) {}\mRightarrow{} (f'[x] = f'[y])))
{}\mRightarrow{} d(f[x])/dx = \mlambda{}x.f'[x] on [-((r1/r(N + 1))), (r1/r(N + 1))]
{}\mRightarrow{} (\mforall{}c:\mBbbR{}
((\mforall{}x:\{x:\mBbbR{}| x \mmember{} [-((r1/r(N + 1))), (r1/r(N + 1))]\} . (|f'[x]| \mleq{} c))
{}\mRightarrow{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [-((r1/r(N + 1))), (r1/r(N + 1))]\} .
(|f[x] - f[y]| \mleq{} (c * |x - y|))))))
6. [-((r1/r(N + 1))), (r1/r(N + 1))] \msubseteq{} (r(-1), r1)
7. \mforall{}c:\mBbbR{}
((\mforall{}x:\{x:\mBbbR{}| x \mmember{} [-((r1/r(N + 1))), (r1/r(N + 1))]\} . (|arcsine\_deriv(x)| \mleq{} c))
{}\mRightarrow{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [-((r1/r(N + 1))), (r1/r(N + 1))]\} .
(|arcsine(x) - arcsine(y)| \mleq{} (c * |x - y|))))
8. 0 < N * (N + 1)
9. r0 < r(N * (N + 1))
10. r0 < rsqrt(r(N * (N + 1)))
11. x : \{x:\mBbbR{}| x \mmember{} [-((r1/r(N + 1))), (r1/r(N + 1))]\}
\mvdash{} |arcsine\_deriv(x)| \mleq{} (r(N + 1)/rsqrt(r(N * (N + 1))))
By
Latex:
(InstLemma `rnexp-rleq` [\mkleeneopen{}|x|\mkleeneclose{};\mkleeneopen{}(r1/r(N + 1))\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{} THENA Auto)
Home
Index