---

Step * 1 of Lemma ip-circle-circle


1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : {c:Point| a # c} 
5. d : Point
6. ∀[p:{p:Point| ab=ap ∧ (||c - p|| ≤ ||c - d||)} ]. ∀[q:{q:Point| cd=cq ∧ (||a - q|| ≤ ||a - b||)} ].
     ∃u,v:{p:Point| ab=ap ∧ cd=cp} . (((||a - q|| < ||a - b||) ∧ (||c - p|| < ||c - d||)) ⇒ u # v)
7. [p] : {p:Point| ab=ap ∧ cd ≥ cp} 
8. ∀[q:{q:Point| cd=cq ∧ (||a - q|| ≤ ||a - b||)} ]
     ∃u,v:{p:Point| ab=ap ∧ cd=cp} . (((||a - q|| < ||a - b||) ∧ (||c - p|| < ||c - d||)) ⇒ u # v)
9. [q] : {q:Point| cd=cq ∧ ab ≥ aq} 
10. u : {p:Point| ab=ap ∧ cd=cp} 
11. ∃v:{p:Point| ab=ap ∧ cd=cp} . (((||a - q|| < ||a - b||) ∧ (||c - p|| < ||c - d||)) ⇒ u # v)
⊢ ∃v:{Point| ((ab=av ∧ cd=cv) ∧ ((ab > aq ∧ cd > cp) ⇒ u # v))}
BY
{ ((D -1 THEN D 0 With ⌜v⌝ ) THEN Auto THEN BackThruSomeHyp THEN EAuto 1) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point
3.  b  :  Point
4.  c  :  \{c:Point|  a  \#  c\} 
5.  d  :  Point
6.  \mforall{}[p:\{p:Point|  ab=ap  \mwedge{}  (||c  -  p||  \mleq{}  ||c  -  d||)\}  ].  \mforall{}[q:\{q:Point|  cd=cq  \mwedge{}  (||a  -  q||  \mleq{}  ||a  -  b||)\}  \000C].
          \mexists{}u,v:\{p:Point|  ab=ap  \mwedge{}  cd=cp\}  .  (((||a  -  q||  <  ||a  -  b||)  \mwedge{}  (||c  -  p||  <  ||c  -  d||))  {}\mRightarrow{}  u  \#  v)
7.  [p]  :  \{p:Point|  ab=ap  \mwedge{}  cd  \mgeq{}  cp\} 
8.  \mforall{}[q:\{q:Point|  cd=cq  \mwedge{}  (||a  -  q||  \mleq{}  ||a  -  b||)\}  ]
          \mexists{}u,v:\{p:Point|  ab=ap  \mwedge{}  cd=cp\}  .  (((||a  -  q||  <  ||a  -  b||)  \mwedge{}  (||c  -  p||  <  ||c  -  d||))  {}\mRightarrow{}  u  \#  v)
9.  [q]  :  \{q:Point|  cd=cq  \mwedge{}  ab  \mgeq{}  aq\} 
10.  u  :  \{p:Point|  ab=ap  \mwedge{}  cd=cp\} 
11.  \mexists{}v:\{p:Point|  ab=ap  \mwedge{}  cd=cp\}  .  (((||a  -  q||  <  ||a  -  b||)  \mwedge{}  (||c  -  p||  <  ||c  -  d||))  {}\mRightarrow{}  u  \#  v)
\mvdash{}  \mexists{}v:\{Point|  ((ab=av  \mwedge{}  cd=cv)  \mwedge{}  ((ab  >  aq  \mwedge{}  cd  >  cp)  {}\mRightarrow{}  u  \#  v))\}


By

---

Latex:
((D  -1  THEN  D  0  With  \mkleeneopen{}v\mkleeneclose{}  )  THEN  Auto  THEN  BackThruSomeHyp  THEN  EAuto  1)

---

Home Index