---

Step * 2 of Lemma ip-line-circle-1


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)))
BY
{ (RepeatFor 4 (MoveToConcl (-1))
   THEN (GenConcl ⌜p - a = pp ∈ Point(rv)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜q - a = qq ∈ Point(rv)⌝⋅ THENA Auto)
   THEN RepUR ``let`` 0
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN (Assert r0 < ||qq - pp|| BY
               EAuto 2)
   THEN (Assert r0 < ||qq - pp||^2 BY
               (BLemma `rnexp-positive` THEN Auto))
   THEN Auto) }

1
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. pp : Point(rv)
9. p - a = pp ∈ Point(rv)
10. qq : Point(rv)
11. q - a = qq ∈ Point(rv)
12. ||pp|| ≤ ||a - b||
13. ||a - b|| ≤ ||qq||
14. pp # qq
15. r0 < ||qq - pp||
16. r0 < ||qq - pp||^2
17. r0 ≤ (((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - ||a - b||^2))
18. ||pp + quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2)*qq - pp|| = ||a - b||
19. ||pp + quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2)*qq - pp|| = ||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:

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||  \mleq{}  ||a  -  b||
9.  ||a  -  b||  \mleq{}  ||q  -  a||
10.  p  -  a  \#  q  -  a
11.  let  v  =  q  -  a  -  p  -  a  in
                (r0  \mleq{}  (((r(2)  *  p  -  a  \mcdot{}  v)  *  r(2)  *  p  -  a  \mcdot{}  v)  -  r(4)
                *  ||v||\^{}2
                *  (||p  -  a||\^{}2  -  ||a  -  b||\^{}2)))
                \mwedge{}  (||p  -  a  +  quadratic1(||v||\^{}2;r(2)  *  p  -  a  \mcdot{}  v;||p  -  a||\^{}2  -  ||a  -  b||\^{}2)*v||  =  ||a  -  b||)
                \mwedge{}  (||p  -  a  +  quadratic2(||v||\^{}2;r(2)  *  p  -  a  \mcdot{}  v;||p  -  a||\^{}2  -  ||a  -  b||\^{}2)*v||  =  ||a  -  b||)
\mvdash{}  \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:
(RepeatFor  4  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}p  -  a  =  pp\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}q  -  a  =  qq\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepUR  ``let``  0
  THEN  RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (Assert  r0  <  ||qq  -  pp||  BY
                          EAuto  2)
  THEN  (Assert  r0  <  ||qq  -  pp||\^{}2  BY
                          (BLemma  `rnexp-positive`  THEN  Auto))
  THEN  Auto)

---

Home Index