---

Step * of Lemma rsin-pi-over-4

rsin((π/r(4))) = (r1/rsqrt(r(2)))
BY
{ (InstLemma `rcos-radd` [⌜(π/r(4))⌝;⌜(π/r(4))⌝]⋅ THENA Auto) }

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

---

Latex:

---

Latex:
rsin((\mpi{}/r(4)))  =  (r1/rsqrt(r(2)))


By

---

Latex:
(InstLemma  `rcos-radd`  [\mkleeneopen{}(\mpi{}/r(4))\mkleeneclose{};\mkleeneopen{}(\mpi{}/r(4))\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index