---

Step * 1 of Lemma rsin-half-pi


1. rsin(π/2(slower))^2 = r1
⊢ rsin(π/2(slower)) = r1
BY
{ (BLemma `square-req-1-iff` THEN Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma  `square-req-1-iff`  THEN  Auto)

---

Home Index