---

Step * of Lemma rv-line-circle-1

∀n:ℕ. ∀a,b,p,q:ℝ^n.
  (a ≠ b
  ⇒ 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:{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)))))
BY
{ (InstLemma `rv-line-circle-0` []
   THEN RepeatFor 5 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN ParallelOp -2
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN Unhide
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,p,q:\mBbbR{}\^{}n.
    (a  \mneq{}  b
    {}\mRightarrow{}  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:\{v:\mBbbR{}\^{}n|  ab=av  \mwedge{}  (\mneg{}(q  \mneq{}  p  \mwedge{}  p  \mneq{}  v  \mwedge{}  (\mneg{}q-p-v)))\} 
                ((d(a;p)  <  d(a;b))  {}\mRightarrow{}  (q-p-v  \mwedge{}  ((d(a;b)  <  d(a;q))  {}\mRightarrow{}  q-u-p)))))


By

---

Latex:
(InstLemma  `rv-line-circle-0`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  Unhide
  THEN  Auto)

---

Home Index