---

Step * 2 1 of Lemma circle-param_wf


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
BY
{ RepeatFor 2 ((nRMul ⌜r1 + (t * t)⌝ 0⋅ THENA Auto)) }

1
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))

---

Latex:

---

Latex:

1.  t  :  \mBbbR{}
2.  r0  \mleq{}  (t  *  t)
3.  r1  \mleq{}  (r1  +  (t  *  t))
4.  r0  <  (r1  +  (t  *  t))
\mvdash{}  (((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


By

---

Latex:
RepeatFor  2  ((nRMul  \mkleeneopen{}r1  +  (t  *  t)\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index