---

Step * 3 of Lemma r2-be-iff


1. u : ℝ^2
2. v : ℝ^2
3. x : ℝ^2
4. ¬(d(u;v) < d(u;x))
5. ¬(d(u;v) < d(x;v))
6. ¬(r2-left(u;x;v) ∨ r2-left(u;v;x))
⊢ u_x_v
BY
{ ((RWO "r2-not-left-right-iff" (-1) THENA Auto)
   THEN (StableCases ⌜u_x_v⌝⋅ THEN Auto)
   THEN D -2
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN (FLemma `rv-be-dist` [-1] THENA Auto)
   THEN (RWO "real-vec-dist-symmetry" (-1) THENA Auto)) }

1
1. u : ℝ^2
2. v : ℝ^2
3. x : ℝ^2
4. ¬(d(u;v) < d(u;x))
5. ¬(d(u;v) < d(x;v))
6. ¬u_x_v
7. ¬u_x_v
8. x_v_u
9. d(u;x) = (d(v;x) + d(u;v))
⊢ False

2
1. u : ℝ^2
2. v : ℝ^2
3. x : ℝ^2
4. ¬(d(u;v) < d(u;x))
5. ¬(d(u;v) < d(x;v))
6. ¬u_x_v
7. ¬u_x_v
8. ¬x_v_u
9. v_u_x
10. d(x;v) = (d(u;v) + d(x;u))
⊢ False

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}\^{}2
2.  v  :  \mBbbR{}\^{}2
3.  x  :  \mBbbR{}\^{}2
4.  \mneg{}(d(u;v)  <  d(u;x))
5.  \mneg{}(d(u;v)  <  d(x;v))
6.  \mneg{}(r2-left(u;x;v)  \mvee{}  r2-left(u;v;x))
\mvdash{}  u\_x\_v


By

---

Latex:
((RWO  "r2-not-left-right-iff"  (-1)  THENA  Auto)
  THEN  (StableCases  \mkleeneopen{}u\_x\_v\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  D  -2
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  (FLemma  `rv-be-dist`  [-1]  THENA  Auto)
  THEN  (RWO  "real-vec-dist-symmetry"  (-1)  THENA  Auto))

---

Home Index