---

Step * 2 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. ¬¬(∃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. d(a;b) = d(u;v)
16. d(a;q) = d(u;w)
17. d(a;q) = (d(a;b) + d(v;w))
⊢ False
BY
{ (Assert r0 ≤ d(v;w) BY
         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. d(a;b) = d(u;v)
16. d(a;q) = d(u;w)
17. d(a;q) = (d(a;b) + d(v;w))
18. r0 ≤ 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.  a  \mneq{}  b
9.  p  \mneq{}  q
10.  d(a;q)  <  d(a;b)
11.  u  :  \mBbbR{}\^{}n
12.  v  :  \mBbbR{}\^{}n
13.  w  :  \mBbbR{}\^{}n
14.  rv-T(n;u;v;w)
15.  d(a;b)  =  d(u;v)
16.  d(a;q)  =  d(u;w)
17.  d(a;q)  =  (d(a;b)  +  d(v;w))
\mvdash{}  False


By

---

Latex:
(Assert  r0  \mleq{}  d(v;w)  BY
              Auto)

---

Home Index