---

Step * of Lemma rv-line-circle

No Annotations
∀n:ℕ. ∀a,b,p,q:ℝ^n.
  (p ≠ q
  ⇒ (∀x:{x:ℝ^n| ap=ax ∧ (¬(a ≠ x ∧ x ≠ b ∧ (¬a-x-b)))} . ∀y:{y:ℝ^n| aq=ay ∧ (¬(a ≠ b ∧ b ≠ y ∧ (¬a-b-y)))} .
        ∃u:{u:ℝ^n| ab=au ∧ (¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p)))} 
         ∃v:{v:ℝ^n| ab=av ∧ (¬(q ≠ p ∧ p ≠ v ∧ (¬q-p-v)))} . (a-x-b ⇒ (q-p-v ∧ (a-b-y ⇒ q-u-p)))))
BY
{ (InstLemma `rv-line-circle-0` [] THEN RepeatFor 6 ((ParallelLast' THENA Auto)) THEN RepeatFor 2 ((D 0 THENA 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))
⇒ (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))))))]))
8. x : {x:ℝ^n| ap=ax ∧ (¬(a ≠ x ∧ x ≠ b ∧ (¬a-x-b)))} 
9. y : {y:ℝ^n| aq=ay ∧ (¬(a ≠ b ∧ b ≠ y ∧ (¬a-b-y)))} 
⊢ ∃u:{u:ℝ^n| ab=au ∧ (¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p)))} 
   ∃v:{v:ℝ^n| ab=av ∧ (¬(q ≠ p ∧ p ≠ v ∧ (¬q-p-v)))} . (a-x-b ⇒ (q-p-v ∧ (a-b-y ⇒ q-u-p)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}a,b,p,q:\mBbbR{}\^{}n.
    (p  \mneq{}  q
    {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}\^{}n|  ap=ax  \mwedge{}  (\mneg{}(a  \mneq{}  x  \mwedge{}  x  \mneq{}  b  \mwedge{}  (\mneg{}a-x-b)))\}  .  \mforall{}y:\{y:\mBbbR{}\^{}n| 
                                                                                                                          aq=ay  \mwedge{}  (\mneg{}(a  \mneq{}  b  \mwedge{}  b  \mneq{}  y  \mwedge{}  (\mneg{}a-b-y)))\}  \000C.
                \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)))\}  .  (a-x-b  {}\mRightarrow{}  (q-p-v  \mwedge{}  (a-b-y  {}\mRightarrow{}  q-u-p)))))


By

---

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

---

Home Index