---

Step * 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. (||a - b|| ≤ ||q - a||)
⇒ (∃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
{ (D -1 THENA Auto) }

1
.....antecedent..... 
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} 
⊢ ||a - b|| ≤ ||q - a||

2
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)])

---

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.  (||a  -  b||  \mleq{}  ||q  -  a||)
{}\mRightarrow{}  (\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:
(D  -1  THENA  Auto)

---

Home Index