---

Step * 1 1 1 1 1 1 1 1 of Lemma rsin-arcsine


1. x : {x:ℝ| x ∈ (r(-1), r1)} 
2. [rmin(rsin(arcsine(x));r0), rmax(rsin(arcsine(x));r0)] ⊆ (r(-1), r1) 
3. [rmin(x;rmin(rsin(arcsine(x));r0)), rmax(x;rmax(rsin(arcsine(x));r0))] ⊆ (r(-1), r1) 
4. [rmin(x;r0), rmax(x;r0)] ⊆ (r(-1), r1) 
5. a : ℝ
6. x_∫-r0 arcsine_deriv(x) dx = a ∈ ℝ
7. rsin(arcsine(x)) ∈ (r(-1), r1)
⊢ (x_∫-rsin(arcsine(x)) arcsine_deriv(x) dx = (a + arcsine(rsin(arcsine(x)))))
⇒ (a = -(arcsine(x)))
⇒ (rsin(arcsine(x)) = x)
BY
{ Assert ⌜x_∫-rsin(arcsine(x)) arcsine_deriv(x) dx ∈ ℝ⌝⋅ }

1
.....assertion..... 
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
2. [rmin(rsin(arcsine(x));r0), rmax(rsin(arcsine(x));r0)] ⊆ (r(-1), r1) 
3. [rmin(x;rmin(rsin(arcsine(x));r0)), rmax(x;rmax(rsin(arcsine(x));r0))] ⊆ (r(-1), r1) 
4. [rmin(x;r0), rmax(x;r0)] ⊆ (r(-1), r1) 
5. a : ℝ
6. x_∫-r0 arcsine_deriv(x) dx = a ∈ ℝ
7. rsin(arcsine(x)) ∈ (r(-1), r1)
⊢ x_∫-rsin(arcsine(x)) arcsine_deriv(x) dx ∈ ℝ

2
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
2. [rmin(rsin(arcsine(x));r0), rmax(rsin(arcsine(x));r0)] ⊆ (r(-1), r1) 
3. [rmin(x;rmin(rsin(arcsine(x));r0)), rmax(x;rmax(rsin(arcsine(x));r0))] ⊆ (r(-1), r1) 
4. [rmin(x;r0), rmax(x;r0)] ⊆ (r(-1), r1) 
5. a : ℝ
6. x_∫-r0 arcsine_deriv(x) dx = a ∈ ℝ
7. rsin(arcsine(x)) ∈ (r(-1), r1)
8. x_∫-rsin(arcsine(x)) arcsine_deriv(x) dx ∈ ℝ
⊢ (x_∫-rsin(arcsine(x)) arcsine_deriv(x) dx = (a + arcsine(rsin(arcsine(x)))))
⇒ (a = -(arcsine(x)))
⇒ (rsin(arcsine(x)) = x)

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\} 
2.  [rmin(rsin(arcsine(x));r0),  rmax(rsin(arcsine(x));r0)]  \msubseteq{}  (r(-1),  r1) 
3.  [rmin(x;rmin(rsin(arcsine(x));r0)),  rmax(x;rmax(rsin(arcsine(x));r0))]  \msubseteq{}  (r(-1),  r1) 
4.  [rmin(x;r0),  rmax(x;r0)]  \msubseteq{}  (r(-1),  r1) 
5.  a  :  \mBbbR{}
6.  x\_\mint{}\msupminus{}r0  arcsine\_deriv(x)  dx  =  a
7.  rsin(arcsine(x))  \mmember{}  (r(-1),  r1)
\mvdash{}  (x\_\mint{}\msupminus{}rsin(arcsine(x))  arcsine\_deriv(x)  dx  =  (a  +  arcsine(rsin(arcsine(x)))))
{}\mRightarrow{}  (a  =  -(arcsine(x)))
{}\mRightarrow{}  (rsin(arcsine(x))  =  x)


By

---

Latex:
Assert  \mkleeneopen{}x\_\mint{}\msupminus{}rsin(arcsine(x))  arcsine\_deriv(x)  dx  \mmember{}  \mBbbR{}\mkleeneclose{}\mcdot{}

---

Home Index