---

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


1. a : ℝ
2. r(-1) < a
3. a < r1
4. x : ℝ
5. c : ℝ
6. |a| ≤ c
7. rsqrt(r1 - a * a) ≤ c
8. r0 ≤ (r1 - a * a)
9. e : {e:ℝ| r0 < e} 
10. (-(π/2), π/2) ⊆ (-∞, ∞) 
11. d(rcos(x))/dx = λx.-(rsin(x)) on (-∞, ∞)
12. d(rsin(x))/dx = λx.rcos(x) on (-∞, ∞)
13. d(-(rsin(x)))/dx = λx.-(rcos(x)) on (-∞, ∞)
14. d(-(rcos(x)))/dx = λx.rsin(x) on (-∞, ∞)
15. c1 : ℝ
16. rmin(arcsine(a);x) ≤ c1
17. c1 ≤ rmax(arcsine(a);x)
18. |arcsine-contraction(a;x) - Σ{(if (k =z 0) then arcsine-contraction(a;arcsine(a))
if (k =z 1) then r1 + ((a * -(rsin(arcsine(a)))) - rsqrt(r1 - a * a) * rcos(arcsine(a)))
if (k =z 2) then r0 + ((a * -(rcos(arcsine(a)))) - rsqrt(r1 - a * a) * -(rsin(arcsine(a))))
else r0 + ((a * -(-(rsin(arcsine(a))))) - rsqrt(r1 - a * a) * -(rcos(arcsine(a))))
fi /r((k)!))
* x - arcsine(a)^k | 0≤k≤2} - (x - c1^2 * (r0 + ((a * -(-(rsin(c1)))) - rsqrt(r1 - a * a) * -(rcos(c1)))/r((2)!)))
* (x - arcsine(a))| ≤ e
19. rcos(arcsine(a)) = rsqrt(r1 - a * a)
20. arcsine-contraction(a;arcsine(a)) = arcsine(a)
⊢ |arcsine-contraction(a;x) - arcsine(a)| ≤ ((c * |x - arcsine(a)|^3) + e)
BY
{ (Assert Σ{(if (k =z 0) then arcsine-contraction(a;arcsine(a))
         if (k =z 1) then r1 + ((a * -(rsin(arcsine(a)))) - rsqrt(r1 - a * a) * rcos(arcsine(a)))
         if (k =z 2) then r0 + ((a * -(rcos(arcsine(a)))) - rsqrt(r1 - a * a) * -(rsin(arcsine(a))))
         else r0 + ((a * -(-(rsin(arcsine(a))))) - rsqrt(r1 - a * a) * -(rcos(arcsine(a))))
         fi /r((k)!))
         * x - arcsine(a)^k | 0≤k≤2}
         = arcsine(a) BY
         (Assert Σ{if (k =z 0) then arcsine(a) else r0 fi  | 0≤k≤2} = arcsine(a) BY
                ((GenConclTerm ⌜arcsine(a)⌝⋅ THENA Auto)
                 THEN (RWO "rsum-split-first" 0 THENA Auto)
                 THEN Reduce 0
                 THEN (RWO "rsum-zero-req" 0 THENA Auto)
                 THEN Try (AutoSplit)
                 THEN nRNorm 0
                 THEN Auto))) }

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

2
1. a : ℝ
2. r(-1) < a
3. a < r1
4. x : ℝ
5. c : ℝ
6. |a| ≤ c
7. rsqrt(r1 - a * a) ≤ c
8. r0 ≤ (r1 - a * a)
9. e : {e:ℝ| r0 < e} 
10. (-(π/2), π/2) ⊆ (-∞, ∞) 
11. d(rcos(x))/dx = λx.-(rsin(x)) on (-∞, ∞)
12. d(rsin(x))/dx = λx.rcos(x) on (-∞, ∞)
13. d(-(rsin(x)))/dx = λx.-(rcos(x)) on (-∞, ∞)
14. d(-(rcos(x)))/dx = λx.rsin(x) on (-∞, ∞)
15. c1 : ℝ
16. rmin(arcsine(a);x) ≤ c1
17. c1 ≤ rmax(arcsine(a);x)
18. |arcsine-contraction(a;x) - Σ{(if (k =z 0) then arcsine-contraction(a;arcsine(a))
if (k =z 1) then r1 + ((a * -(rsin(arcsine(a)))) - rsqrt(r1 - a * a) * rcos(arcsine(a)))
if (k =z 2) then r0 + ((a * -(rcos(arcsine(a)))) - rsqrt(r1 - a * a) * -(rsin(arcsine(a))))
else r0 + ((a * -(-(rsin(arcsine(a))))) - rsqrt(r1 - a * a) * -(rcos(arcsine(a))))
fi /r((k)!))
* x - arcsine(a)^k | 0≤k≤2} - (x - c1^2 * (r0 + ((a * -(-(rsin(c1)))) - rsqrt(r1 - a * a) * -(rcos(c1)))/r((2)!)))
* (x - arcsine(a))| ≤ e
19. rcos(arcsine(a)) = rsqrt(r1 - a * a)
20. arcsine-contraction(a;arcsine(a)) = arcsine(a)
21. Σ{(if (k =z 0) then arcsine-contraction(a;arcsine(a))
if (k =z 1) then r1 + ((a * -(rsin(arcsine(a)))) - rsqrt(r1 - a * a) * rcos(arcsine(a)))
if (k =z 2) then r0 + ((a * -(rcos(arcsine(a)))) - rsqrt(r1 - a * a) * -(rsin(arcsine(a))))
else r0 + ((a * -(-(rsin(arcsine(a))))) - rsqrt(r1 - a * a) * -(rcos(arcsine(a))))
fi /r((k)!))
* x - arcsine(a)^k | 0≤k≤2}
= arcsine(a)
⊢ |arcsine-contraction(a;x) - arcsine(a)| ≤ ((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.  |a|  \mleq{}  c
7.  rsqrt(r1  -  a  *  a)  \mleq{}  c
8.  r0  \mleq{}  (r1  -  a  *  a)
9.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
10.  (-(\mpi{}/2),  \mpi{}/2)  \msubseteq{}  (-\minfty{},  \minfty{}) 
11.  d(rcos(x))/dx  =  \mlambda{}x.-(rsin(x))  on  (-\minfty{},  \minfty{})
12.  d(rsin(x))/dx  =  \mlambda{}x.rcos(x)  on  (-\minfty{},  \minfty{})
13.  d(-(rsin(x)))/dx  =  \mlambda{}x.-(rcos(x))  on  (-\minfty{},  \minfty{})
14.  d(-(rcos(x)))/dx  =  \mlambda{}x.rsin(x)  on  (-\minfty{},  \minfty{})
15.  c1  :  \mBbbR{}
16.  rmin(arcsine(a);x)  \mleq{}  c1
17.  c1  \mleq{}  rmax(arcsine(a);x)
18.  |arcsine-contraction(a;x)  -  \mSigma{}\{(if  (k  =\msubz{}  0)  then  arcsine-contraction(a;arcsine(a))
if  (k  =\msubz{}  1)  then  r1  +  ((a  *  -(rsin(arcsine(a))))  -  rsqrt(r1  -  a  *  a)  *  rcos(arcsine(a)))
if  (k  =\msubz{}  2)  then  r0  +  ((a  *  -(rcos(arcsine(a))))  -  rsqrt(r1  -  a  *  a)  *  -(rsin(arcsine(a))))
else  r0  +  ((a  *  -(-(rsin(arcsine(a)))))  -  rsqrt(r1  -  a  *  a)  *  -(rcos(arcsine(a))))
fi  /r((k)!))
*  x  -  arcsine(a)\^{}k  |  0\mleq{}k\mleq{}2\}  -  (x  -  c1\^{}2
*  (r0  +  ((a  *  -(-(rsin(c1))))  -  rsqrt(r1  -  a  *  a)  *  -(rcos(c1)))/r((2)!)))
*  (x  -  arcsine(a))|  \mleq{}  e
19.  rcos(arcsine(a))  =  rsqrt(r1  -  a  *  a)
20.  arcsine-contraction(a;arcsine(a))  =  arcsine(a)
\mvdash{}  |arcsine-contraction(a;x)  -  arcsine(a)|  \mleq{}  ((c  *  |x  -  arcsine(a)|\^{}3)  +  e)


By

---

Latex:
(Assert  \mSigma{}\{(if  (k  =\msubz{}  0)  then  arcsine-contraction(a;arcsine(a))
              if  (k  =\msubz{}  1)  then  r1  +  ((a  *  -(rsin(arcsine(a))))  -  rsqrt(r1  -  a  *  a)  *  rcos(arcsine(a)))
              if  (k  =\msubz{}  2)  then  r0  +  ((a  *  -(rcos(arcsine(a))))  -  rsqrt(r1  -  a  *  a)  *  -(rsin(arcsine(a))))
              else  r0  +  ((a  *  -(-(rsin(arcsine(a)))))  -  rsqrt(r1  -  a  *  a)  *  -(rcos(arcsine(a))))
              fi  /r((k)!))
              *  x  -  arcsine(a)\^{}k  |  0\mleq{}k\mleq{}2\}
              =  arcsine(a)  BY
              (Assert  \mSigma{}\{if  (k  =\msubz{}  0)  then  arcsine(a)  else  r0  fi    |  0\mleq{}k\mleq{}2\}  =  arcsine(a)  BY
                            ((GenConclTerm  \mkleeneopen{}arcsine(a)\mkleeneclose{}\mcdot{}  THENA  Auto)
                              THEN  (RWO  "rsum-split-first"  0  THENA  Auto)
                              THEN  Reduce  0
                              THEN  (RWO  "rsum-zero-req"  0  THENA  Auto)
                              THEN  Try  (AutoSplit)
                              THEN  nRNorm  0
                              THEN  Auto)))

---

Home Index