---

Step * 2 2 of Lemma ip-line-circle


1. rv : InnerProductSpace
2. a : Point(rv)
3. b : {b:Point(rv)| a # b} 
4. p : {p:Point(rv)| ab ≥ ap} 
5. q : {q:Point(rv)| p # q ∧ aq ≥ ab} 
6. ∃u:{u:Point(rv)| ab=au ∧ q_u_p} 
    ∃v:{v:Point(rv)| ab=av ∧ q_p_v} . ((||a - p|| < ||a - b||) ⇒ (p # v ∧ ((||a - b|| < ||a - q||) ⇒ q # u)))
⊢ ∃u:{u:Point(rv)| ab=au ∧ q_u_p} . (∃v:Point(rv) [(ab=av ∧ q_p_v)])
BY
{ (ParallelLast THEN D -1 THEN D 0 With ⌜v⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  \{b:Point(rv)|  a  \#  b\} 
4.  p  :  \{p:Point(rv)|  ab  \mgeq{}  ap\} 
5.  q  :  \{q:Point(rv)|  p  \#  q  \mwedge{}  aq  \mgeq{}  ab\} 
6.  \mexists{}u:\{u:Point(rv)|  ab=au  \mwedge{}  q\_u\_p\} 
        \mexists{}v:\{v:Point(rv)|  ab=av  \mwedge{}  q\_p\_v\} 
          ((||a  -  p||  <  ||a  -  b||)  {}\mRightarrow{}  (p  \#  v  \mwedge{}  ((||a  -  b||  <  ||a  -  q||)  {}\mRightarrow{}  q  \#  u)))
\mvdash{}  \mexists{}u:\{u:Point(rv)|  ab=au  \mwedge{}  q\_u\_p\}  .  (\mexists{}v:Point(rv)  [(ab=av  \mwedge{}  q\_p\_v)])


By

---

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

---

Home Index