---

Step * 1 1 1 1 2 1 1 of Lemma implies-isometry-lemma4


1. rv : InnerProductSpace
2. x : Point(rv)
3. y : Point(rv)
4. v : ℝ
5. ||x - y|| < (r(2) * v)
6. r0 < ||x - y||
7. x # y
8. x - x + (v/||x - y||)*y - x ≡ (v/||x - y||)*x - y
9. y - y + (v/||x - y||)*x - y ≡ (v/||x - y||)*y - x
10. r0 < v
⊢ ∃z:Point(rv). ((||z - x|| = v) ∧ (||z - y|| = v))
BY
{ ((Assert r0 < (v/||x - y||) BY
          (nRMul ⌜||x - y||⌝ 0⋅ THEN Auto))
   THEN (InstLemma `ip-circle-circle-lemma3` 
         [⌜rv⌝;⌜x⌝;⌜x + (v/||x - y||)*y - x⌝;⌜y⌝;⌜y + (v/||x - y||)*x - y⌝
         ;⌜x + (v/||x - y||)*y - x⌝;⌜y + (v/||x - y||)*x - y⌝]⋅
         THENA (Auto THEN MemTypeCD THEN Auto THEN Try ((Unfold `ip-congruent` 0 THEN Auto)))
         )
   ) }

1
1. rv : InnerProductSpace
2. x : Point(rv)
3. y : Point(rv)
4. v : ℝ
5. ||x - y|| < (r(2) * v)
6. r0 < ||x - y||
7. x # y
8. x - x + (v/||x - y||)*y - x ≡ (v/||x - y||)*x - y
9. y - y + (v/||x - y||)*x - y ≡ (v/||x - y||)*y - x
10. r0 < v
11. r0 < (v/||x - y||)
12. xx + (v/||x - y||)*y - x=xx + (v/||x - y||)*y - x
⊢ ||y - x + (v/||x - y||)*y - x|| ≤ ||y - y + (v/||x - y||)*x - y||

2
1. rv : InnerProductSpace
2. x : Point(rv)
3. y : Point(rv)
4. v : ℝ
5. ||x - y|| < (r(2) * v)
6. r0 < ||x - y||
7. x # y
8. x - x + (v/||x - y||)*y - x ≡ (v/||x - y||)*x - y
9. y - y + (v/||x - y||)*x - y ≡ (v/||x - y||)*y - x
10. r0 < v
11. r0 < (v/||x - y||)
12. yy + (v/||x - y||)*x - y=yy + (v/||x - y||)*x - y
⊢ ||x - y + (v/||x - y||)*x - y|| ≤ ||x - x + (v/||x - y||)*y - x||

3
1. rv : InnerProductSpace
2. x : Point(rv)
3. y : Point(rv)
4. v : ℝ
5. ||x - y|| < (r(2) * v)
6. r0 < ||x - y||
7. x # y
8. x - x + (v/||x - y||)*y - x ≡ (v/||x - y||)*x - y
9. y - y + (v/||x - y||)*x - y ≡ (v/||x - y||)*y - x
10. r0 < v
11. r0 < (v/||x - y||)
12. ∃u,v@0:{p:Point(rv)| xx + (v/||x - y||)*y - x=xp ∧ yy + (v/||x - y||)*x - y=yp} 
     (((||x - y + (v/||x - y||)*x - y|| < ||x - x + (v/||x - y||)*y - x||)
     ∧ (||y - x + (v/||x - y||)*y - x|| < ||y - y + (v/||x - y||)*x - y||))
     ⇒ u # v@0)
⊢ ∃z:Point(rv). ((||z - x|| = v) ∧ (||z - y|| = v))

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  Point(rv)
3.  y  :  Point(rv)
4.  v  :  \mBbbR{}
5.  ||x  -  y||  <  (r(2)  *  v)
6.  r0  <  ||x  -  y||
7.  x  \#  y
8.  x  -  x  +  (v/||x  -  y||)*y  -  x  \mequiv{}  (v/||x  -  y||)*x  -  y
9.  y  -  y  +  (v/||x  -  y||)*x  -  y  \mequiv{}  (v/||x  -  y||)*y  -  x
10.  r0  <  v
\mvdash{}  \mexists{}z:Point(rv).  ((||z  -  x||  =  v)  \mwedge{}  (||z  -  y||  =  v))


By

---

Latex:
((Assert  r0  <  (v/||x  -  y||)  BY
                (nRMul  \mkleeneopen{}||x  -  y||\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  (InstLemma  `ip-circle-circle-lemma3` 
              [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x  +  (v/||x  -  y||)*y  -  x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}y  +  (v/||x  -  y||)*x  -  y\mkleeneclose{}
              ;\mkleeneopen{}x  +  (v/||x  -  y||)*y  -  x\mkleeneclose{};\mkleeneopen{}y  +  (v/||x  -  y||)*x  -  y\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  MemTypeCD  THEN  Auto  THEN  Try  ((Unfold  `ip-congruent`  0  THEN  Auto)))
              )
  )

---

Home Index