---

Step * 1 1 1 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) + (r(2) * t1 * t1 * t1)) = ((r(2) * t2) + (r(2) * t2 * t2 * 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))
11. (r(2) * t1 * t2 * t2) = (r(2) * t1 * t1 * t1)
12. (r(2) * t2 * t2 * t2) = (r(2) * t1 * t1 * t2)
⊢ t1 = t2
BY
{ (Assert (t1 * (r(2) + (r(2) * t1 * t1))) = (t2 * (r(2) + (r(2) * t2 * t2))) BY
         Auto) }

1
1. t1 : ℝ
2. t2 : ℝ
3. (r(2) * t2 * t2) = (r(2) * t1 * t1)
4. ((r(2) * t1) + (r(2) * t1 * t1 * t1)) = ((r(2) * t2) + (r(2) * t2 * t2 * 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))
11. (r(2) * t1 * t2 * t2) = (r(2) * t1 * t1 * t1)
12. (r(2) * t2 * t2 * t2) = (r(2) * t1 * t1 * t2)
13. (t1 * (r(2) + (r(2) * t1 * t1))) = (t2 * (r(2) + (r(2) * 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)  +  (r(2)  *  t1  *  t1  *  t1))  =  ((r(2)  *  t2)  +  (r(2)  *  t2  *  t2  *  t2))
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))
11.  (r(2)  *  t1  *  t2  *  t2)  =  (r(2)  *  t1  *  t1  *  t1)
12.  (r(2)  *  t2  *  t2  *  t2)  =  (r(2)  *  t1  *  t1  *  t2)
\mvdash{}  t1  =  t2


By

---

Latex:
(Assert  (t1  *  (r(2)  +  (r(2)  *  t1  *  t1)))  =  (t2  *  (r(2)  +  (r(2)  *  t2  *  t2)))  BY
              Auto)

---

Home Index