---

Step * of Lemma rsin-half-pi

rsin(π/2(slower)) = r1
BY
{ ((InstLemma `rsin-rcos-pythag` [⌜π/2(slower)⌝]⋅ THENA Auto)
   THEN (RWO "rcos-half-pi" (-1) THENA Auto)
   THEN (RWO "rnexp0" (-1) THENA Auto)
   THEN (nRNorm (-1) THENA Auto)) }

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

---

Latex:

---

Latex:
rsin(\mpi{}/2(slower))  =  r1


By

---

Latex:
((InstLemma  `rsin-rcos-pythag`  [\mkleeneopen{}\mpi{}/2(slower)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "rcos-half-pi"  (-1)  THENA  Auto)
  THEN  (RWO  "rnexp0"  (-1)  THENA  Auto)
  THEN  (nRNorm  (-1)  THENA  Auto))

---

Home Index