---

Step * 1 1 of Lemma rv-line-circle-0


1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. p : ℝ^n
5. q : ℝ^n
6. p ≠ q
7. d(a;p) ≤ d(a;b)
8. d(a;b) ≤ d(a;q)
9. ((d(a;p) < d(a;b)) ⇒ (||p - a|| < d(a;b))) ∧ (||p - a|| ≤ d(a;b))
10. ((d(a;b) < d(a;q)) ⇒ (d(a;b) < ||q - a||)) ∧ (d(a;b) ≤ ||q - a||)
⊢ ∃u:{u:ℝ^n| ab=au} 
   (real-vec-be(n;q;u;p)
   ∧ (∃v:{v:ℝ^n| ab=av} 
       (real-vec-be(n;q;p;v)
       ∧ ((d(a;p) < d(a;b)) ⇒ (q-p-v ∧ ((d(a;b) < d(a;q)) ⇒ q-u-p)))
       ∧ ((d(a;p) = d(a;b))
         ⇒ ((u ≠ v ⇒ ((req-vec(n;u;p) ∧ (r0 < p - a⋅q - p)) ∨ (req-vec(n;v;p) ∧ (p - a⋅q - p < r0))))
            ∧ (req-vec(n;u;v) ⇒ ((p - a⋅q - p = r0) ∧ req-vec(n;u;p))))))))
BY
{ ((Assert p - a ≠ q - a BY
          (ParallelOp 6 THEN RWO "real-vec-dist-translation" 0 THEN Auto))
   THEN (InstLemma `rv-line-circle-lemma` [⌜n⌝;⌜d(a;b)⌝;⌜p - a⌝;⌜q - a⌝]⋅ THENA Auto)
   THEN RepeatFor 4 (MoveToConcl (-1))
   THEN (GenConcl ⌜p - a = pp ∈ ℝ^n⌝⋅ THENA Auto)
   THEN (GenConcl ⌜q - a = qq ∈ ℝ^n⌝⋅ THENA Auto)
   THEN RepUR ``let`` 0
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN (Assert r0 < ||qq - pp|| BY
               ((Fold `real-vec-dist` 0 THENA Auto) THEN RWO "real-vec-dist-symmetry" 0 THEN Auto))
   THEN (Assert r0 < ||qq - pp||^2 BY
               (BLemma `rnexp-positive` THEN Auto))
   THEN Auto) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. p : ℝ^n
5. q : ℝ^n
6. p ≠ q
7. d(a;p) ≤ d(a;b)
8. d(a;b) ≤ d(a;q)
9. pp : ℝ^n
10. p - a = pp ∈ ℝ^n
11. qq : ℝ^n
12. q - a = qq ∈ ℝ^n
13. (d(a;p) < d(a;b)) ⇒ (||pp|| < d(a;b))
14. ||pp|| ≤ d(a;b)
15. (d(a;b) < d(a;q)) ⇒ (d(a;b) < ||qq||)
16. d(a;b) ≤ ||qq||
17. pp ≠ qq
18. r0 < ||qq - pp||
19. r0 < ||qq - pp||^2
20. r0 ≤ (((r(2) * pp⋅qq - pp) * r(2) * pp⋅qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - d(a;b)^2))
21. ||pp + quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp|| = d(a;b)
22. ||pp + quadratic2(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp|| = d(a;b)
⊢ ∃u:{u:ℝ^n| ab=au} 
   (real-vec-be(n;q;u;p)
   ∧ (∃v:{v:ℝ^n| ab=av} 
       (real-vec-be(n;q;p;v)
       ∧ ((d(a;p) < d(a;b)) ⇒ (q-p-v ∧ ((d(a;b) < d(a;q)) ⇒ q-u-p)))
       ∧ ((d(a;p) = d(a;b))
         ⇒ ((u ≠ v ⇒ ((req-vec(n;u;p) ∧ (r0 < pp⋅q - p)) ∨ (req-vec(n;v;p) ∧ (pp⋅q - p < r0))))
            ∧ (req-vec(n;u;v) ⇒ ((pp⋅q - p = r0) ∧ req-vec(n;u;p))))))))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  p  :  \mBbbR{}\^{}n
5.  q  :  \mBbbR{}\^{}n
6.  p  \mneq{}  q
7.  d(a;p)  \mleq{}  d(a;b)
8.  d(a;b)  \mleq{}  d(a;q)
9.  ((d(a;p)  <  d(a;b))  {}\mRightarrow{}  (||p  -  a||  <  d(a;b)))  \mwedge{}  (||p  -  a||  \mleq{}  d(a;b))
10.  ((d(a;b)  <  d(a;q))  {}\mRightarrow{}  (d(a;b)  <  ||q  -  a||))  \mwedge{}  (d(a;b)  \mleq{}  ||q  -  a||)
\mvdash{}  \mexists{}u:\{u:\mBbbR{}\^{}n|  ab=au\} 
      (real-vec-be(n;q;u;p)
      \mwedge{}  (\mexists{}v:\{v:\mBbbR{}\^{}n|  ab=av\} 
              (real-vec-be(n;q;p;v)
              \mwedge{}  ((d(a;p)  <  d(a;b))  {}\mRightarrow{}  (q-p-v  \mwedge{}  ((d(a;b)  <  d(a;q))  {}\mRightarrow{}  q-u-p)))
              \mwedge{}  ((d(a;p)  =  d(a;b))
                  {}\mRightarrow{}  ((u  \mneq{}  v
                        {}\mRightarrow{}  ((req-vec(n;u;p)  \mwedge{}  (r0  <  p  -  a\mcdot{}q  -  p))  \mvee{}  (req-vec(n;v;p)  \mwedge{}  (p  -  a\mcdot{}q  -  p  <  r0))))
                        \mwedge{}  (req-vec(n;u;v)  {}\mRightarrow{}  ((p  -  a\mcdot{}q  -  p  =  r0)  \mwedge{}  req-vec(n;u;p))))))))


By

---

Latex:
((Assert  p  -  a  \mneq{}  q  -  a  BY
                (ParallelOp  6  THEN  RWO  "real-vec-dist-translation"  0  THEN  Auto))
  THEN  (InstLemma  `rv-line-circle-lemma`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}d(a;b)\mkleeneclose{};\mkleeneopen{}p  -  a\mkleeneclose{};\mkleeneopen{}q  -  a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  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
                          ((Fold  `real-vec-dist`  0  THENA  Auto)  THEN  RWO  "real-vec-dist-symmetry"  0  THEN  Auto))
  THEN  (Assert  r0  <  ||qq  -  pp||\^{}2  BY
                          (BLemma  `rnexp-positive`  THEN  Auto))
  THEN  Auto)

---

Home Index