---

Step * 1 1 1 2 1 1 of Lemma arcsine-approx_wf


1. a : ℝ
2. (r(-3)/r(4)) < a
3. a < (r(3)/r(4))
4. n : ℕ+
5. j : ℕ
6. (2 * n) ≤ 10^3^j
7. r(-1) < r0
8. (r(3)/r(4)) < r1
9. r(-1) < (r(-3)/r(4))
10. a ∈ {a:ℝ| (r(-1) < a) ∧ (a < r1)} 
11. v : ℤ
12. z : ℝ
13. (r(v))/2 * 4 * n = z ∈ ℝ
14. |z - arcsine-contraction^j(a)| ≤ (r(2)/r(4 * n))
15. ¬(r0 < a)
16. a ≤ r0
17. -(a) ∈ {x:ℝ| (r(-1) < x) ∧ (x < r1)} 
18. (a - arcsine(a)) = -(-(a) - arcsine(-(a)))
⊢ |-(a) - arcsine(-(a))|^3^j ≤ (r1/r(2 * n))
BY
{ (StableCases ⌜r0 < -(a)⌝⋅ THENA Auto) }

1
1. a : ℝ
2. (r(-3)/r(4)) < a
3. a < (r(3)/r(4))
4. n : ℕ+
5. j : ℕ
6. (2 * n) ≤ 10^3^j
7. r(-1) < r0
8. (r(3)/r(4)) < r1
9. r(-1) < (r(-3)/r(4))
10. a ∈ {a:ℝ| (r(-1) < a) ∧ (a < r1)} 
11. v : ℤ
12. z : ℝ
13. (r(v))/2 * 4 * n = z ∈ ℝ
14. |z - arcsine-contraction^j(a)| ≤ (r(2)/r(4 * n))
15. ¬(r0 < a)
16. a ≤ r0
17. -(a) ∈ {x:ℝ| (r(-1) < x) ∧ (x < r1)} 
18. (a - arcsine(a)) = -(-(a) - arcsine(-(a)))
19. r0 < -(a)
⊢ |-(a) - arcsine(-(a))|^3^j ≤ (r1/r(2 * n))

2
1. a : ℝ
2. (r(-3)/r(4)) < a
3. a < (r(3)/r(4))
4. n : ℕ+
5. j : ℕ
6. (2 * n) ≤ 10^3^j
7. r(-1) < r0
8. (r(3)/r(4)) < r1
9. r(-1) < (r(-3)/r(4))
10. a ∈ {a:ℝ| (r(-1) < a) ∧ (a < r1)} 
11. v : ℤ
12. z : ℝ
13. (r(v))/2 * 4 * n = z ∈ ℝ
14. |z - arcsine-contraction^j(a)| ≤ (r(2)/r(4 * n))
15. ¬(r0 < a)
16. a ≤ r0
17. -(a) ∈ {x:ℝ| (r(-1) < x) ∧ (x < r1)} 
18. (a - arcsine(a)) = -(-(a) - arcsine(-(a)))
19. ¬(r0 < -(a))
⊢ |-(a) - arcsine(-(a))|^3^j ≤ (r1/r(2 * n))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  (r(-3)/r(4))  <  a
3.  a  <  (r(3)/r(4))
4.  n  :  \mBbbN{}\msupplus{}
5.  j  :  \mBbbN{}
6.  (2  *  n)  \mleq{}  10\^{}3\^{}j
7.  r(-1)  <  r0
8.  (r(3)/r(4))  <  r1
9.  r(-1)  <  (r(-3)/r(4))
10.  a  \mmember{}  \{a:\mBbbR{}|  (r(-1)  <  a)  \mwedge{}  (a  <  r1)\} 
11.  v  :  \mBbbZ{}
12.  z  :  \mBbbR{}
13.  (r(v))/2  *  4  *  n  =  z
14.  |z  -  arcsine-contraction\^{}j(a)|  \mleq{}  (r(2)/r(4  *  n))
15.  \mneg{}(r0  <  a)
16.  a  \mleq{}  r0
17.  -(a)  \mmember{}  \{x:\mBbbR{}|  (r(-1)  <  x)  \mwedge{}  (x  <  r1)\} 
18.  (a  -  arcsine(a))  =  -(-(a)  -  arcsine(-(a)))
\mvdash{}  |-(a)  -  arcsine(-(a))|\^{}3\^{}j  \mleq{}  (r1/r(2  *  n))


By

---

Latex:
(StableCases  \mkleeneopen{}r0  <  -(a)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index