---

Step * 1 4 of Lemma arcsine-bounds

.....antecedent..... 
1. x : {x:ℝ| x ∈ (r(-1), r1)} 
⊢ λx.rsin(x)(-(π/2)) < x
BY
{ ((RepUR ``r-ap`` 0 THEN (RWO "rsin-rminus" 0 THENM RWW  "rsin-halfpi" 0) THEN Auto)
   THEN All Reduce
   THEN (Assert r(-1) < x BY
               Auto)
   THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  x  :  \{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\} 
\mvdash{}  \mlambda{}x.rsin(x)(-(\mpi{}/2))  <  x


By

---

Latex:
((RepUR  ``r-ap``  0  THEN  (RWO  "rsin-rminus"  0  THENM  RWW    "rsin-halfpi"  0)  THEN  Auto)
  THEN  All  Reduce
  THEN  (Assert  r(-1)  <  x  BY
                          Auto)
  THEN  Auto)

---

Home Index