---

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


1. t1 : ℝ
2. t2 : ℝ
3. (r1 - t1 * t1/r1 + (t1 * t1)) = (r1 - t2 * t2/r1 + (t2 * t2))
4. (r(2) * t1/r1 + (t1 * t1)) = (r(2) * t2/r1 + (t2 * t2))
⊢ t1 = t2
BY
{ (((Assert r0 ≤ (t1 * t1) BY
           Auto)
    THEN (Assert r1 ≤ (r1 + (t1 * t1)) BY
                Auto)
    THEN (Assert r0 < (r1 + (t1 * t1)) BY
                (RWO  "-1<" 0 THEN Auto)))
   THEN (Assert r0 ≤ (t2 * t2) BY
               Auto)
   THEN (Assert r1 ≤ (r1 + (t2 * t2)) BY
               Auto)
   THEN (Assert r0 < (r1 + (t2 * t2)) BY
               (RWO  "-1<" 0 THEN Auto))) }

1
1. t1 : ℝ
2. t2 : ℝ
3. (r1 - t1 * t1/r1 + (t1 * t1)) = (r1 - t2 * t2/r1 + (t2 * t2))
4. (r(2) * t1/r1 + (t1 * t1)) = (r(2) * t2/r1 + (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))
⊢ t1 = t2

---

Latex:

---

Latex:

1.  t1  :  \mBbbR{}
2.  t2  :  \mBbbR{}
3.  (r1  -  t1  *  t1/r1  +  (t1  *  t1))  =  (r1  -  t2  *  t2/r1  +  (t2  *  t2))
4.  (r(2)  *  t1/r1  +  (t1  *  t1))  =  (r(2)  *  t2/r1  +  (t2  *  t2))
\mvdash{}  t1  =  t2


By

---

Latex:
(((Assert  r0  \mleq{}  (t1  *  t1)  BY
                  Auto)
    THEN  (Assert  r1  \mleq{}  (r1  +  (t1  *  t1))  BY
                            Auto)
    THEN  (Assert  r0  <  (r1  +  (t1  *  t1))  BY
                            (RWO    "-1<"  0  THEN  Auto)))
  THEN  (Assert  r0  \mleq{}  (t2  *  t2)  BY
                          Auto)
  THEN  (Assert  r1  \mleq{}  (r1  +  (t2  *  t2))  BY
                          Auto)
  THEN  (Assert  r0  <  (r1  +  (t2  *  t2))  BY
                          (RWO    "-1<"  0  THEN  Auto)))

---

Home Index