---

Step * 1 1 1 of Lemma circle-param-one-one


1. t1 : ℝ
2. t2 : ℝ
3. ((r1 - t1 * t1) * (r1 + (t2 * t2))) = ((r1 - t2 * t2) * (r1 + (t1 * t1)))
4. ((r(2) * t1) * (r1 + (t2 * t2))) = ((r(2) * t2) * (r1 + (t1 * t1)))
5. r0 ≤ (t1 * t1)
6. r1 ≤ (r1 + (t1 * t1))
7. r0 < (r1 + (t1 * t1))
8. r0 ≤ (t2 * t2)
9. r1 ≤ (r1 + (t2 * t2))
10. r0 < (r1 + (t2 * t2))
⊢ t1 = t2
BY
{ (nRAdd ⌜(t1 * t1 * t2 * t2) + (t1 * t1) + ((t2 * t2) - r1)⌝ 3⋅ THENA Auto) }

1
1. t1 : ℝ
2. t2 : ℝ
3. (r(2) * t2 * t2) = (r(2) * t1 * t1)
4. ((r(2) * t1) * (r1 + (t2 * t2))) = ((r(2) * t2) * (r1 + (t1 * t1)))
5. r0 ≤ (t1 * t1)
6. r1 ≤ (r1 + (t1 * t1))
7. r0 < (r1 + (t1 * t1))
8. r0 ≤ (t2 * t2)
9. r1 ≤ (r1 + (t2 * t2))
10. r0 < (r1 + (t2 * t2))
⊢ t1 = t2

---

Latex:

---

Latex:

1.  t1  :  \mBbbR{}
2.  t2  :  \mBbbR{}
3.  ((r1  -  t1  *  t1)  *  (r1  +  (t2  *  t2)))  =  ((r1  -  t2  *  t2)  *  (r1  +  (t1  *  t1)))
4.  ((r(2)  *  t1)  *  (r1  +  (t2  *  t2)))  =  ((r(2)  *  t2)  *  (r1  +  (t1  *  t1)))
5.  r0  \mleq{}  (t1  *  t1)
6.  r1  \mleq{}  (r1  +  (t1  *  t1))
7.  r0  <  (r1  +  (t1  *  t1))
8.  r0  \mleq{}  (t2  *  t2)
9.  r1  \mleq{}  (r1  +  (t2  *  t2))
10.  r0  <  (r1  +  (t2  *  t2))
\mvdash{}  t1  =  t2


By

---

Latex:
(nRAdd  \mkleeneopen{}(t1  *  t1  *  t2  *  t2)  +  (t1  *  t1)  +  ((t2  *  t2)  -  r1)\mkleeneclose{}  3\mcdot{}  THENA  Auto)

---

Home Index