---

Step * of Lemma rv-line-circle-0

No Annotations
∀n:ℕ. ∀a,b,p,q:ℝ^n.
  (p ≠ q
  ⇒ (d(a;p) ≤ d(a;b))
  ⇒ (d(a;b) ≤ d(a;q))
  ⇒ (∃u:{u:ℝ^n| ab=au ∧ (¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p)))} 
       (∃v:ℝ^n [(ab=av
               ∧ (¬(q ≠ p ∧ p ≠ v ∧ (¬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
{ (Auto
   THEN Assert ⌜∃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))))))))⌝⋅
   ) }

1
.....assertion..... 
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)
⊢ ∃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))))))))

2
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. ∃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))))))))
⊢ ∃u:{u:ℝ^n| ab=au ∧ (¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p)))} 
   (∃v:ℝ^n [(ab=av
           ∧ (¬(q ≠ p ∧ p ≠ v ∧ (¬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))))))])

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}a,b,p,q:\mBbbR{}\^{}n.
    (p  \mneq{}  q
    {}\mRightarrow{}  (d(a;p)  \mleq{}  d(a;b))
    {}\mRightarrow{}  (d(a;b)  \mleq{}  d(a;q))
    {}\mRightarrow{}  (\mexists{}u:\{u:\mBbbR{}\^{}n|  ab=au  \mwedge{}  (\mneg{}(q  \mneq{}  u  \mwedge{}  u  \mneq{}  p  \mwedge{}  (\mneg{}q-u-p)))\} 
              (\mexists{}v:\mBbbR{}\^{}n  [(ab=av
                              \mwedge{}  (\mneg{}(q  \mneq{}  p  \mwedge{}  p  \mneq{}  v  \mwedge{}  (\mneg{}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:
(Auto
  THEN  Assert  \mkleeneopen{}\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))))))))\mkleeneclose{}\mcdot{}
  )

---

Home Index