---

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


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
BY
{ (nRNorm 4 THENA Auto) }

1
1. t1 : ℝ
2. t2 : ℝ
3. (r(2) * t2 * t2) = (r(2) * t1 * t1)
4. ((r(2) * t1) + (r(2) * t1 * t2 * t2)) = ((r(2) * t2) + (r(2) * t1 * t1 * t2))
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.  (r(2)  *  t2  *  t2)  =  (r(2)  *  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:
(nRNorm  4  THENA  Auto)

---

Home Index