---

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


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
BY
{ (MoveToConcl (-2) THEN GenConclTerm ⌜(r1/rsqrt(r(2)))⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-2)  THEN  GenConclTerm  \mkleeneopen{}(r1/rsqrt(r(2)))\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index