---

Step * 2 1 1 of Lemma circle-param_wf


1. t : ℝ
2. r0 ≤ (t * t)
3. r1 ≤ (r1 + (t * t))
4. r0 < (r1 + (t * t))
⊢ (r1 + (r(2) * t * t) + (t * t * t * t)) = (r1 + (r(2) * t * t) + (t * t * t * t))
BY
{ Auto }

---

Latex:

---

Latex:

1.  t  :  \mBbbR{}
2.  r0  \mleq{}  (t  *  t)
3.  r1  \mleq{}  (r1  +  (t  *  t))
4.  r0  <  (r1  +  (t  *  t))
\mvdash{}  (r1  +  (r(2)  *  t  *  t)  +  (t  *  t  *  t  *  t))  =  (r1  +  (r(2)  *  t  *  t)  +  (t  *  t  *  t  *  t))


By

---

Latex:
Auto

---

Home Index