---

Step * 2 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. ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ap=uv ∧ ab=uw))
7. q : ℝ^n
8. ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ab=uv ∧ aq=uw))
9. a ≠ b
10. p ≠ q
⊢ ¬(d(a;q) < d(a;b))
BY
{ (ParallelOp -3
   THEN (D 0 THENA Auto)
   THEN ExRepD
   THEN (RWO "rv-T-iff<" (-3) THENA Auto)
   THEN (FLemma `rv-T-dist` [-3] THENA Auto)) }

1
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. ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ap=uv ∧ ab=uw))
7. q : ℝ^n
8. a ≠ b
9. p ≠ q
10. d(a;q) < d(a;b)
11. u : ℝ^n
12. v : ℝ^n
13. w : ℝ^n
14. rv-T(n;u;v;w)
15. ab=uv
16. aq=uw
17. d(u;w) = (d(u;v) + d(v;w))
⊢ False

---

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.  \mneg{}\mneg{}(\mexists{}u,v,w:\mBbbR{}\^{}n.  ((\mneg{}(u  \mneq{}  v  \mwedge{}  v  \mneq{}  w  \mwedge{}  (\mneg{}u-v-w)))  \mwedge{}  ap=uv  \mwedge{}  ab=uw))
7.  q  :  \mBbbR{}\^{}n
8.  \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))
9.  a  \mneq{}  b
10.  p  \mneq{}  q
\mvdash{}  \mneg{}(d(a;q)  <  d(a;b))


By

---

Latex:
(ParallelOp  -3
  THEN  (D  0  THENA  Auto)
  THEN  ExRepD
  THEN  (RWO  "rv-T-iff<"  (-3)  THENA  Auto)
  THEN  (FLemma  `rv-T-dist`  [-3]  THENA  Auto))

---

Home Index