---

Step * 1 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. k : ℕ4
16. x1 : {a:ℝ| True} 
17. y : {a:ℝ| True} 
18. x1 = y
⊢ if (k =z 0) then arcsine-contraction(a;x1)
if (k =z 1) then r1 + ((a * -(rsin(x1))) - rsqrt(r1 - a * a) * rcos(x1))
if (k =z 2) then r0 + ((a * -(rcos(x1))) - rsqrt(r1 - a * a) * -(rsin(x1)))
else r0 + ((a * -(-(rsin(x1)))) - rsqrt(r1 - a * a) * -(rcos(x1)))
fi 
= if (k =z 0) then arcsine-contraction(a;y)
  if (k =z 1) then r1 + ((a * -(rsin(y))) - rsqrt(r1 - a * a) * rcos(y))
  if (k =z 2) then r0 + ((a * -(rcos(y))) - rsqrt(r1 - a * a) * -(rsin(y)))
  else r0 + ((a * -(-(rsin(y)))) - rsqrt(r1 - a * a) * -(rcos(y)))
  fi 
BY
{ (IntSegCases (-4) THEN Reduce 0 THEN Auto THEN Try (Unfold `arcsine-contraction` 0) THEN RWO "-2" 0 THEN Auto) }

---

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.  k  :  \mBbbN{}4
16.  x1  :  \{a:\mBbbR{}|  True\} 
17.  y  :  \{a:\mBbbR{}|  True\} 
18.  x1  =  y
\mvdash{}  if  (k  =\msubz{}  0)  then  arcsine-contraction(a;x1)
if  (k  =\msubz{}  1)  then  r1  +  ((a  *  -(rsin(x1)))  -  rsqrt(r1  -  a  *  a)  *  rcos(x1))
if  (k  =\msubz{}  2)  then  r0  +  ((a  *  -(rcos(x1)))  -  rsqrt(r1  -  a  *  a)  *  -(rsin(x1)))
else  r0  +  ((a  *  -(-(rsin(x1))))  -  rsqrt(r1  -  a  *  a)  *  -(rcos(x1)))
fi 
=  if  (k  =\msubz{}  0)  then  arcsine-contraction(a;y)
    if  (k  =\msubz{}  1)  then  r1  +  ((a  *  -(rsin(y)))  -  rsqrt(r1  -  a  *  a)  *  rcos(y))
    if  (k  =\msubz{}  2)  then  r0  +  ((a  *  -(rcos(y)))  -  rsqrt(r1  -  a  *  a)  *  -(rsin(y)))
    else  r0  +  ((a  *  -(-(rsin(y))))  -  rsqrt(r1  -  a  *  a)  *  -(rcos(y)))
    fi 


By

---

Latex:
(IntSegCases  (-4)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (Unfold  `arcsine-contraction`  0)
  THEN  RWO  "-2"  0
  THEN  Auto)

---

Home Index