---

Step * 1 5 of Lemma arcsine-bounds

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

---

Latex:

---

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


By

---

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

---

Home Index