---

Step * 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) * 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))
11. (r(2) * t1 * t2 * t2) = (r(2) * t1 * t1 * t1)
⊢ t1 = t2
BY
{ ((Assert ((r(2) * t2 * t2) * t2) = ((r(2) * t1 * t1) * t2) BY
          (BLemma `rmul_functionality` THEN Auto))
   THEN (nRNorm (-1) THENA Auto)
   THEN (RWO "-1<" 4 THENA 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)
⊢ 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)  *  t1  *  t1  *  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)
\mvdash{}  t1  =  t2


By

---

Latex:
((Assert  ((r(2)  *  t2  *  t2)  *  t2)  =  ((r(2)  *  t1  *  t1)  *  t2)  BY
                (BLemma  `rmul\_functionality`  THEN  Auto))
  THEN  (nRNorm  (-1)  THENA  Auto)
  THEN  (RWO  "-1<"  4  THENA  Auto))

---

Home Index