---

Step * 2 of Lemma circle-param_wf

.....set predicate..... 
1. t : ℝ
2. r0 ≤ (t * t)
3. r1 ≤ (r1 + (t * t))
4. r0 < (r1 + (t * t))
⊢ r2-unit-circle(circle-param(t))
BY
{ (RepUR ``r2-unit-circle circle-param`` 0 THEN (RWO "rnexp2" 0 THENA Auto)) }

1
1. t : ℝ
2. r0 ≤ (t * t)
3. r1 ≤ (r1 + (t * t))
4. r0 < (r1 + (t * t))
⊢ (((r1 - t * t/r1 + (t * t)) * (r1 - t * t/r1 + (t * t))) + ((r(2) * t/r1 + (t * t)) * (r(2) * t/r1 + (t * t)))) = r1

---

Latex:

---

Latex:
.....set  predicate..... 
1.  t  :  \mBbbR{}
2.  r0  \mleq{}  (t  *  t)
3.  r1  \mleq{}  (r1  +  (t  *  t))
4.  r0  <  (r1  +  (t  *  t))
\mvdash{}  r2-unit-circle(circle-param(t))


By

---

Latex:
(RepUR  ``r2-unit-circle  circle-param``  0  THEN  (RWO  "rnexp2"  0  THENA  Auto))

---

Home Index