---

Step * 1 1 of Lemma rsin-pi-over-4


1. rcos((π/r(4)) + (π/r(4))) = ((rcos((π/r(4))) * rcos((π/r(4)))) - rsin((π/r(4))) * rsin((π/r(4))))
2. rcos((π/r(4)) + (π/r(4))) = rcos(π/2)
⊢ rsin((π/r(4))) = (r1/rsqrt(r(2)))
BY
{ ((RWW "-1 rcos-halfpi rnexp2<" (-2) THENA Auto) THEN (InstLemma `rsin-rcos-pythag` [⌜(π/r(4))⌝]⋅ THENA Auto)) }

1
1. r0 = (rcos((π/r(4)))^2 - rsin((π/r(4)))^2)
2. rcos((π/r(4)) + (π/r(4))) = rcos(π/2)
3. (rsin((π/r(4)))^2 + rcos((π/r(4)))^2) = r1
⊢ rsin((π/r(4))) = (r1/rsqrt(r(2)))

---

Latex:

---

Latex:

1.  rcos((\mpi{}/r(4))  +  (\mpi{}/r(4)))  =  ((rcos((\mpi{}/r(4)))  *  rcos((\mpi{}/r(4))))  -  rsin((\mpi{}/r(4)))  *  rsin((\mpi{}/r(4))))
2.  rcos((\mpi{}/r(4))  +  (\mpi{}/r(4)))  =  rcos(\mpi{}/2)
\mvdash{}  rsin((\mpi{}/r(4)))  =  (r1/rsqrt(r(2)))


By

---

Latex:
((RWW  "-1  rcos-halfpi  rnexp2<"  (-2)  THENA  Auto)
  THEN  (InstLemma  `rsin-rcos-pythag`  [\mkleeneopen{}(\mpi{}/r(4))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index