---

Step * 1 1 of Lemma rsin-half-pi


1. rsin(π/2(slower))^2 = r1
⊢ rsin(π/2(slower)) ≠ -(r1)
BY
{ (OrRight THEN Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(OrRight  THEN  Auto)

---

Home Index