---

Step * of Lemma rtan-pi-over-4

rtan((π/r(4))) = r1
BY
{ ((Assert r0 < rsqrt(r(2)) BY
          EAuto 2)
   THEN (Assert r0 < (r1/rsqrt(r(2))) BY
               (nRMul ⌜rsqrt(r(2))⌝ 0⋅ THEN Auto))
   THEN (Assert r0 < rcos((π/r(4))) BY
               (RWO "rcos-pi-over-4" 0 THEN Auto))
   THEN RepUR ``rtan`` 0
   THEN (RWO "rcos-pi-over-4" 0 THENA Auto)
   THEN (RWO "rsin-pi-over-4" 0 THENA Auto)) }

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

---

Latex:

---

Latex:
rtan((\mpi{}/r(4)))  =  r1


By

---

Latex:
((Assert  r0  <  rsqrt(r(2))  BY
                EAuto  2)
  THEN  (Assert  r0  <  (r1/rsqrt(r(2)))  BY
                          (nRMul  \mkleeneopen{}rsqrt(r(2))\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  (Assert  r0  <  rcos((\mpi{}/r(4)))  BY
                          (RWO  "rcos-pi-over-4"  0  THEN  Auto))
  THEN  RepUR  ``rtan``  0
  THEN  (RWO  "rcos-pi-over-4"  0  THENA  Auto)
  THEN  (RWO  "rsin-pi-over-4"  0  THENA  Auto))

---

Home Index