---

Step * 1 3 1 2 1 2 1 1 of Lemma arcsine-contraction-Taylor


1. a : ℝ
2. r(-1) < a
3. a < r1
4. x : ℝ
5. c : ℝ
6. r0 ≤ a
7. a ≤ c
8. rsqrt(r1 - a * a) ≤ c
9. r0 ≤ (r1 - a * a)
10. e : {e:ℝ| r0 < e} 
11. (-(π/2), π/2) ⊆ (-∞, ∞) 
12. d(rcos(x))/dx = λx.-(rsin(x)) on (-∞, ∞)
13. d(rsin(x))/dx = λx.rcos(x) on (-∞, ∞)
14. d(-(rsin(x)))/dx = λx.-(rcos(x)) on (-∞, ∞)
15. d(-(rcos(x)))/dx = λx.rsin(x) on (-∞, ∞)
16. c1 : ℝ
17. rmin(arcsine(a);x) ≤ c1
18. c1 ≤ rmax(arcsine(a);x)
19. rcos(arcsine(a)) = rsqrt(r1 - a * a)
20. arcsine-contraction(a;arcsine(a)) = arcsine(a)
21. z : ℝ
22. (arcsine-contraction(a;x) - arcsine(a)) = z ∈ ℝ
⊢ (|z - (x - c1^2 * (r0 + ((a * -(-(rsin(c1)))) - rsqrt(r1 - a * a) * -(rcos(c1)))/r((2)!))) * (x - arcsine(a))| ≤ e)
⇒ (|z| ≤ ((c * |x - arcsine(a)|^3) + e))
BY
{ (Assert |(r0 + ((a * -(-(rsin(c1)))) - rsqrt(r1 - a * a) * -(rcos(c1)))/r((2)!))| ≤ c BY
         ((Subst' (2)! ~ 2 0 THENA Auto)
          THEN (RWO "rabs-rdiv" 0 THENA (Auto THEN RWO  "rabs-of-nonneg" 0 THEN Auto))
          THEN (Assert |r(2)| = r(2) BY
                      (RWO "rabs-of-nonneg" 0 THEN Auto))
          THEN (RWO "-1" 0 THENA (Auto THEN RWO "rabs-of-nonneg" 0 THEN Auto))
          THEN nRMul ⌜r(2)⌝ 0⋅
          THEN (RWO "r-triangle-inequality" 0 THENA Auto)
          THEN RWO "rabs-rmul" 0
          THEN Auto)) }

1
1. a : ℝ
2. r(-1) < a
3. a < r1
4. x : ℝ
5. c : ℝ
6. r0 ≤ a
7. a ≤ c
8. rsqrt(r1 - a * a) ≤ c
9. r0 ≤ (r1 - a * a)
10. e : {e:ℝ| r0 < e} 
11. (-(π/2), π/2) ⊆ (-∞, ∞) 
12. d(rcos(x))/dx = λx.-(rsin(x)) on (-∞, ∞)
13. d(rsin(x))/dx = λx.rcos(x) on (-∞, ∞)
14. d(-(rsin(x)))/dx = λx.-(rcos(x)) on (-∞, ∞)
15. d(-(rcos(x)))/dx = λx.rsin(x) on (-∞, ∞)
16. c1 : ℝ
17. rmin(arcsine(a);x) ≤ c1
18. c1 ≤ rmax(arcsine(a);x)
19. rcos(arcsine(a)) = rsqrt(r1 - a * a)
20. arcsine-contraction(a;arcsine(a)) = arcsine(a)
21. z : ℝ
22. (arcsine-contraction(a;x) - arcsine(a)) = z ∈ ℝ
23. |r(2)| = r(2)
⊢ ((|rcos(c1)| * |rsqrt(r1 + -(a * a))|) + (|rsin(c1)| * |a|)) ≤ (r(2) * c)

2
1. a : ℝ
2. r(-1) < a
3. a < r1
4. x : ℝ
5. c : ℝ
6. r0 ≤ a
7. a ≤ c
8. rsqrt(r1 - a * a) ≤ c
9. r0 ≤ (r1 - a * a)
10. e : {e:ℝ| r0 < e} 
11. (-(π/2), π/2) ⊆ (-∞, ∞) 
12. d(rcos(x))/dx = λx.-(rsin(x)) on (-∞, ∞)
13. d(rsin(x))/dx = λx.rcos(x) on (-∞, ∞)
14. d(-(rsin(x)))/dx = λx.-(rcos(x)) on (-∞, ∞)
15. d(-(rcos(x)))/dx = λx.rsin(x) on (-∞, ∞)
16. c1 : ℝ
17. rmin(arcsine(a);x) ≤ c1
18. c1 ≤ rmax(arcsine(a);x)
19. rcos(arcsine(a)) = rsqrt(r1 - a * a)
20. arcsine-contraction(a;arcsine(a)) = arcsine(a)
21. z : ℝ
22. (arcsine-contraction(a;x) - arcsine(a)) = z ∈ ℝ
23. |(r0 + ((a * -(-(rsin(c1)))) - rsqrt(r1 - a * a) * -(rcos(c1)))/r((2)!))| ≤ c
⊢ (|z - (x - c1^2 * (r0 + ((a * -(-(rsin(c1)))) - rsqrt(r1 - a * a) * -(rcos(c1)))/r((2)!))) * (x - arcsine(a))| ≤ e)
⇒ (|z| ≤ ((c * |x - arcsine(a)|^3) + e))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  r(-1)  <  a
3.  a  <  r1
4.  x  :  \mBbbR{}
5.  c  :  \mBbbR{}
6.  r0  \mleq{}  a
7.  a  \mleq{}  c
8.  rsqrt(r1  -  a  *  a)  \mleq{}  c
9.  r0  \mleq{}  (r1  -  a  *  a)
10.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
11.  (-(\mpi{}/2),  \mpi{}/2)  \msubseteq{}  (-\minfty{},  \minfty{}) 
12.  d(rcos(x))/dx  =  \mlambda{}x.-(rsin(x))  on  (-\minfty{},  \minfty{})
13.  d(rsin(x))/dx  =  \mlambda{}x.rcos(x)  on  (-\minfty{},  \minfty{})
14.  d(-(rsin(x)))/dx  =  \mlambda{}x.-(rcos(x))  on  (-\minfty{},  \minfty{})
15.  d(-(rcos(x)))/dx  =  \mlambda{}x.rsin(x)  on  (-\minfty{},  \minfty{})
16.  c1  :  \mBbbR{}
17.  rmin(arcsine(a);x)  \mleq{}  c1
18.  c1  \mleq{}  rmax(arcsine(a);x)
19.  rcos(arcsine(a))  =  rsqrt(r1  -  a  *  a)
20.  arcsine-contraction(a;arcsine(a))  =  arcsine(a)
21.  z  :  \mBbbR{}
22.  (arcsine-contraction(a;x)  -  arcsine(a))  =  z
\mvdash{}  (|z  -  (x  -  c1\^{}2  *  (r0  +  ((a  *  -(-(rsin(c1))))  -  rsqrt(r1  -  a  *  a)  *  -(rcos(c1)))/r((2)!)))
*  (x  -  arcsine(a))|  \mleq{}  e)
{}\mRightarrow{}  (|z|  \mleq{}  ((c  *  |x  -  arcsine(a)|\^{}3)  +  e))


By

---

Latex:
(Assert  |(r0  +  ((a  *  -(-(rsin(c1))))  -  rsqrt(r1  -  a  *  a)  *  -(rcos(c1)))/r((2)!))|  \mleq{}  c  BY
              ((Subst'  (2)!  \msim{}  2  0  THENA  Auto)
                THEN  (RWO  "rabs-rdiv"  0  THENA  (Auto  THEN  RWO    "rabs-of-nonneg"  0  THEN  Auto))
                THEN  (Assert  |r(2)|  =  r(2)  BY
                                        (RWO  "rabs-of-nonneg"  0  THEN  Auto))
                THEN  (RWO  "-1"  0  THENA  (Auto  THEN  RWO  "rabs-of-nonneg"  0  THEN  Auto))
                THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}
                THEN  (RWO  "r-triangle-inequality"  0  THENA  Auto)
                THEN  RWO  "rabs-rmul"  0
                THEN  Auto))

---

Home Index