---

Step * 1 2 of Lemma rcos-pi-over-4


1. r0 < rsqrt(r(2))
2. ((r1/rsqrt(r(2)))^2 + rcos((π/r(4)))^2) = r1
3. r0 < rcos((π/r(4)))
4. rcos((π/r(4))) = rsqrt((r1/r(2)))
⊢ rcos((π/r(4))) = (r1/rsqrt(r(2)))
BY
{ ((RWO "-1" 0 THENA Auto) THEN (RWO "rsqrt-rdiv<" 0 THEN Auto) THEN BLemma `rdiv_functionality` THEN Auto) }

---

Latex:

---

Latex:

1.  r0  <  rsqrt(r(2))
2.  ((r1/rsqrt(r(2)))\^{}2  +  rcos((\mpi{}/r(4)))\^{}2)  =  r1
3.  r0  <  rcos((\mpi{}/r(4)))
4.  rcos((\mpi{}/r(4)))  =  rsqrt((r1/r(2)))
\mvdash{}  rcos((\mpi{}/r(4)))  =  (r1/rsqrt(r(2)))


By

---

Latex:
((RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "rsqrt-rdiv<"  0  THEN  Auto)
  THEN  BLemma  `rdiv\_functionality`
  THEN  Auto)

---

Home Index