---

Step * 1 1 1 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)))
⊢ rcos((π/r(4)))^2 = (r1/r(2))
BY
{ ((Assert rsqrt(r(2))^2 = r(2) BY
          Auto)
   THEN (Assert rsqrt(r(2))^2 ≠ r0 BY
               (RWO "-1" 0 THEN Auto))
   THEN (Assert (r1/rsqrt(r(2)))^2 = (r1/r(2)) BY
               (RWO "rnexp-rdiv<" 0 THEN Auto THEN BLemma `rdiv_functionality` THEN Auto))) }

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

---

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


By

---

Latex:
((Assert  rsqrt(r(2))\^{}2  =  r(2)  BY
                Auto)
  THEN  (Assert  rsqrt(r(2))\^{}2  \mneq{}  r0  BY
                          (RWO  "-1"  0  THEN  Auto))
  THEN  (Assert  (r1/rsqrt(r(2)))\^{}2  =  (r1/r(2))  BY
                          (RWO  "rnexp-rdiv<"  0  THEN  Auto  THEN  BLemma  `rdiv\_functionality`  THEN  Auto)))

---

Home Index