---

Step * of Lemma rcos-pi-over-4

rcos((π/r(4))) = (r1/rsqrt(r(2)))
BY
{ ((Assert r0 < rsqrt(r(2)) BY
          (UseWitness ⌜4⌝⋅ THEN Auto))
   THEN (InstLemma `rsin-rcos-pythag` [⌜(π/r(4))⌝]⋅ THENA Auto)
   THEN (RWO "rsin-pi-over-4" (-1) THENA Auto)) }

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

---

Latex:

---

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


By

---

Latex:
((Assert  r0  <  rsqrt(r(2))  BY
                (UseWitness  \mkleeneopen{}4\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (InstLemma  `rsin-rcos-pythag`  [\mkleeneopen{}(\mpi{}/r(4))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "rsin-pi-over-4"  (-1)  THENA  Auto))

---

Home Index