---

Step * of Lemma r2-be-iff

No Annotations
∀u,v,x:ℝ^2.  (u_x_v ⇐⇒ ((¬(d(u;v) < d(u;x))) ∧ (¬(d(u;v) < d(x;v)))) ∧ (¬(r2-left(u;x;v) ∨ r2-left(u;v;x))))
BY
{ (Auto
   THEN Try (((FLemma `rv-be-dist` [-1] THENA Auto) THEN (RWO "-1" 0 THENA Auto) THEN (D 0 THENA Auto)))
   THEN Try (((RWO "r2-not-left-right-iff" 0 THENM D 0) THEN Auto))) }

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

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

3
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

---

Latex:

---

Latex:
No  Annotations
\mforall{}u,v,x:\mBbbR{}\^{}2.
    (u\_x\_v  \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}(d(u;v)  <  d(u;x)))  \mwedge{}  (\mneg{}(d(u;v)  <  d(x;v))))  \mwedge{}  (\mneg{}(r2-left(u;x;v)  \mvee{}  r2-left(u;v;x))))


By

---

Latex:
(Auto
  THEN  Try  (((FLemma  `rv-be-dist`  [-1]  THENA  Auto)
                        THEN  (RWO  "-1"  0  THENA  Auto)
                        THEN  (D  0  THENA  Auto)))
  THEN  Try  (((RWO  "r2-not-left-right-iff"  0  THENM  D  0)  THEN  Auto)))

---

Home Index