---

Step * of Lemma ip-line-circle-1

No Annotations
∀rv:InnerProductSpace. ∀a,b,p,q:Point(rv).
  (a # b
  ⇒ p # q
  ⇒ (||p - a|| ≤ ||a - b||)
  ⇒ (||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)))))
BY
{ (Auto
   THEN (Assert ⌜p - a # q - a⌝⋅
        THENM (InstLemma `ip-line-circle-lemma` [⌜rv⌝;⌜||a - b||⌝;⌜p - a⌝;⌜q - a⌝]⋅ THENA Auto)
        )
   ) }

1
.....assertion..... 
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. p : Point(rv)
5. q : Point(rv)
6. a # b
7. p # q
8. ||p - a|| ≤ ||a - b||
9. ||a - b|| ≤ ||q - a||
⊢ p - a # q - a

2
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. p : Point(rv)
5. q : Point(rv)
6. a # b
7. p # q
8. ||p - a|| ≤ ||a - b||
9. ||a - b|| ≤ ||q - a||
10. p - a # q - a
11. let v = q - a - p - a in
        (r0 ≤ (((r(2) * p - a ⋅ v) * r(2) * p - a ⋅ v) - r(4) * ||v||^2 * (||p - a||^2 - ||a - b||^2)))
        ∧ (||p - a + quadratic1(||v||^2;r(2) * p - a ⋅ v;||p - a||^2 - ||a - b||^2)*v|| = ||a - b||)
        ∧ (||p - a + quadratic2(||v||^2;r(2) * p - a ⋅ v;||p - a||^2 - ||a - b||^2)*v|| = ||a - b||)
⊢ ∃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)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,p,q:Point(rv).
    (a  \#  b
    {}\mRightarrow{}  p  \#  q
    {}\mRightarrow{}  (||p  -  a||  \mleq{}  ||a  -  b||)
    {}\mRightarrow{}  (||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)))))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}p  -  a  \#  q  -  a\mkleeneclose{}\mcdot{}
            THENM  (InstLemma  `ip-line-circle-lemma`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}||a  -  b||\mkleeneclose{};\mkleeneopen{}p  -  a\mkleeneclose{};\mkleeneopen{}q  -  a\mkleeneclose{}]\mcdot{}  THENA  Auto)
            )
  )

---

Home Index