---

Step * of Lemma ip-circle-circle

∀rv:InnerProductSpace. ∀a,b:Point. ∀c:{c:Point| a # c} . ∀d:Point.
  ∀[p:{p:Point| ab=ap ∧ cd ≥ cp} ]. ∀[q:{q:Point| cd=cq ∧ ab ≥ aq} ].
    ∃u:{u:Point| ab=au ∧ cd=cu} . (∃v:{Point| ((ab=av ∧ cd=cv) ∧ ((ab > aq ∧ cd > cp) ⇒ u # v))})
BY
{ (InstLemma `ip-circle-circle-lemma3` []
   THEN RepeatFor 5 (ParallelLast')
   THEN RepeatFor 2 ((ParallelLast THENA (D -1 THEN MemTypeCD THEN EAuto 1)))
   THEN ParallelLast') }

1
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))}

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  a  \#  c\}  .  \mforall{}d:Point.
    \mforall{}[p:\{p:Point|  ab=ap  \mwedge{}  cd  \mgeq{}  cp\}  ].  \mforall{}[q:\{q:Point|  cd=cq  \mwedge{}  ab  \mgeq{}  aq\}  ].
        \mexists{}u:\{u:Point|  ab=au  \mwedge{}  cd=cu\}  .  (\mexists{}v:\{Point|  ((ab=av  \mwedge{}  cd=cv)  \mwedge{}  ((ab  >  aq  \mwedge{}  cd  >  cp)  {}\mRightarrow{}  u  \#  v))\})


By

---

Latex:
(InstLemma  `ip-circle-circle-lemma3`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  RepeatFor  2  ((ParallelLast  THENA  (D  -1  THEN  MemTypeCD  THEN  EAuto  1)))
  THEN  ParallelLast')

---

Home Index