---

Step * of Lemma arcsine_functionality_wrt_rless

∀x,y:{x:ℝ| x ∈ (r(-1), r1)} .  ((x < y) ⇒ (arcsine(x) < arcsine(y)))
BY
{ (Auto
   THEN (InstLemma `derivative-implies-strictly-increasing` 
         [⌜(r(-1), r1)⌝;⌜λ2x.arcsine(x)⌝;⌜λ2x.arcsine_deriv(x)⌝]⋅
         THENA (Auto THEN RepUR ``iproper left-endpoint right-endpoint endpoints`` 0 THEN Auto)
         )
   ) }

1
.....antecedent..... 
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
2. y : {x:ℝ| x ∈ (r(-1), r1)} 
3. x < y
⊢ arcsine_deriv(x) continuous for x ∈ (r(-1), r1)

2
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
2. y : {x:ℝ| x ∈ (r(-1), r1)} 
3. x < y
4. x1 : {x:ℝ| x ∈ (r(-1), r1)} 
⊢ r0 < arcsine_deriv(x1)

3
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
2. y : {x:ℝ| x ∈ (r(-1), r1)} 
3. x < y
4. arcsine(x) strictly-increasing for x ∈ (r(-1), r1)
⊢ arcsine(x) < arcsine(y)

---

Latex:

---

Latex:
\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\}  .    ((x  <  y)  {}\mRightarrow{}  (arcsine(x)  <  arcsine(y)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `derivative-implies-strictly-increasing` 
              [\mkleeneopen{}(r(-1),  r1)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.arcsine(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.arcsine\_deriv(x)\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RepUR  ``iproper  left-endpoint  right-endpoint  endpoints``  0  THEN  Auto)
              )
  )

---

Home Index