---

Step * 2 1 2 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. 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||
20. quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) ∈ [r0, r1]
21. (quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) ≤ r0)
∧ ((||a - p|| < ||a - b||) ⇒ (quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) < r0))
⊢ ∃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 ⌜quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = t ∈ ℝ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = s ∈ ℝ⌝⋅ THENA Auto)
   THEN (Assert ∀X:Point(rv). pp + X ≡ p + X - a BY
               (Auto
                THEN (Assert p - a = pp ∈ Point(rv) BY
                            Hypothesis)
                THEN (RWO "-1<" 0 THENA Auto)
                THEN RealVecEqual
                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. t : ℝ
19. quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = t ∈ ℝ
20. s : ℝ
21. quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = s ∈ ℝ
22. ∀X:Point(rv). pp + X ≡ p + X - a
⊢ (||pp + t*qq - pp|| = ||a - b||)
⇒ (||pp + s*qq - pp|| = ||a - b||)
⇒ (t ∈ [r0, r1])
⇒ ((s ≤ r0) ∧ ((||a - p|| < ||a - b||) ⇒ (s < r0)))
⇒ (∃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.  pp  :  Point(rv)
9.  p  -  a  =  pp
10.  qq  :  Point(rv)
11.  q  -  a  =  qq
12.  ||pp||  \mleq{}  ||a  -  b||
13.  ||a  -  b||  \mleq{}  ||qq||
14.  pp  \#  qq
15.  r0  <  ||qq  -  pp||
16.  r0  <  ||qq  -  pp||\^{}2
17.  r0  \mleq{}  (((r(2)  *  pp  \mcdot{}  qq  -  pp)  *  r(2)  *  pp  \mcdot{}  qq  -  pp)  -  r(4)
*  ||qq  -  pp||\^{}2
*  (||pp||\^{}2  -  ||a  -  b||\^{}2))
18.  ||pp  +  quadratic1(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)*qq  -  pp||
=  ||a  -  b||
19.  ||pp  +  quadratic2(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)*qq  -  pp||
=  ||a  -  b||
20.  quadratic1(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)  \mmember{}  [r0,  r1]
21.  (quadratic2(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)  \mleq{}  r0)
\mwedge{}  ((||a  -  p||  <  ||a  -  b||)
    {}\mRightarrow{}  (quadratic2(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)  <  r0))
\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{}quadratic1(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)  =  t\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  (GenConcl  \mkleeneopen{}quadratic2(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)  =  s\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  (Assert  \mforall{}X:Point(rv).  pp  +  X  \mequiv{}  p  +  X  -  a  BY
                          (Auto
                            THEN  (Assert  p  -  a  =  pp  BY
                                                    Hypothesis)
                            THEN  (RWO  "-1<"  0  THENA  Auto)
                            THEN  RealVecEqual
                            THEN  Auto)))

---

Home Index