---

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


1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. ∀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)))))
5. p : ℝ^n
6. q : ℝ^n
7. ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ab=uv ∧ aq=uw))
8. a ≠ b
9. p ≠ q
10. u : ℝ^n
11. v : ℝ^n
12. w : ℝ^n
13. rv-T(n;u;v;w)
14. d(a;p) = d(u;v)
15. d(a;b) = d(u;w)
16. d(a;b) = (d(a;p) + d(v;w))
17. r0 ≤ d(v;w)
18. (d(a;p) + d(v;w)) < d(a;p)
⊢ False
BY
{ (nRAdd ⌜-(d(a;p))⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  \mforall{}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)))))
5.  p  :  \mBbbR{}\^{}n
6.  q  :  \mBbbR{}\^{}n
7.  \mneg{}\mneg{}(\mexists{}u,v,w:\mBbbR{}\^{}n.  ((\mneg{}(u  \mneq{}  v  \mwedge{}  v  \mneq{}  w  \mwedge{}  (\mneg{}u-v-w)))  \mwedge{}  ab=uv  \mwedge{}  aq=uw))
8.  a  \mneq{}  b
9.  p  \mneq{}  q
10.  u  :  \mBbbR{}\^{}n
11.  v  :  \mBbbR{}\^{}n
12.  w  :  \mBbbR{}\^{}n
13.  rv-T(n;u;v;w)
14.  d(a;p)  =  d(u;v)
15.  d(a;b)  =  d(u;w)
16.  d(a;b)  =  (d(a;p)  +  d(v;w))
17.  r0  \mleq{}  d(v;w)
18.  (d(a;p)  +  d(v;w))  <  d(a;p)
\mvdash{}  False


By

---

Latex:
(nRAdd  \mkleeneopen{}-(d(a;p))\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index