---

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

.....antecedent..... 
1. r0 < rsqrt(r(2))
2. ((r1/rsqrt(r(2)))^2 + rcos((π/r(4)))^2) = r1
3. r0 < rcos((π/r(4)))
⊢ (rcos((π/r(4))) * rcos((π/r(4)))) = (r1/r(2))
BY
{ (RWO "rnexp2<" 0 THENA Auto) }

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

---

Latex:

---

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


By

---

Latex:
(RWO  "rnexp2<"  0  THENA  Auto)

---

Home Index