---

Step * 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))))
⊢ rsin((π/r(4))) = (r1/rsqrt(r(2)))
BY
{ (Assert rcos((π/r(4)) + (π/r(4))) = rcos(π/2) BY
         (BLemma `rcos_functionality`
          THEN Auto
          THEN RepUR ``pi`` 0
          THEN nRMul ⌜r(4)⌝ 0⋅
          THEN RWO "int-rmul-req" 0
          THEN Auto)) }

1
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)))

---

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))))
\mvdash{}  rsin((\mpi{}/r(4)))  =  (r1/rsqrt(r(2)))


By

---

Latex:
(Assert  rcos((\mpi{}/r(4))  +  (\mpi{}/r(4)))  =  rcos(\mpi{}/2)  BY
              (BLemma  `rcos\_functionality`
                THEN  Auto
                THEN  RepUR  ``pi``  0
                THEN  nRMul  \mkleeneopen{}r(4)\mkleeneclose{}  0\mcdot{}
                THEN  RWO  "int-rmul-req"  0
                THEN  Auto))

---

Home Index