---

Step * 1 1 1 of Lemma rsin-half-pi


1. rsin(π/2(slower))^2 = r1
⊢ -(r1) < rsin(π/2(slower))
BY
{ (D 0 With ⌜5⌝  THENA Auto) }

1
1. rsin(π/2(slower))^2 = r1
⊢ (-(r1) 5) + 4 < rsin(π/2(slower)) 5

---

Latex:

---

Latex:

1.  rsin(\mpi{}/2(slower))\^{}2  =  r1
\mvdash{}  -(r1)  <  rsin(\mpi{}/2(slower))


By

---

Latex:
(D  0  With  \mkleeneopen{}5\mkleeneclose{}    THENA  Auto)

---

Home Index