---

Step * 1 1 of Lemma r2-compass-compass


1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. a ≠ c
5. d : ℝ^2
6. p : ℝ^2
7. q : ℝ^2
8. d(a;b) = d(a;p)
9. ¬¬(∃w:ℝ^2. (c_w_d ∧ (d(c;w) = d(c;p))))
10. d(c;d) = d(c;q)
11. ¬¬(∃w:ℝ^2. (a_w_b ∧ (d(a;w) = d(a;q))))
12. d(a;b) = d(a;p)
13. d(c;d) = d(c;q)
⊢ d(c;p) ≤ d(c;d)
BY
{ ((StableCases ⌜∃w:ℝ^2. (c_w_d ∧ (d(c;w) = d(c;p)))⌝⋅ THEN Auto)
   THEN ExRepD
   THEN (FLemma `rv-be-dist` [-2] THENA Auto)
   THEN (RWW "-1 -2" 0 THENA Auto)
   THEN nRAdd ⌜-(d(c;p))⌝ 0⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  c  :  \mBbbR{}\^{}2
4.  a  \mneq{}  c
5.  d  :  \mBbbR{}\^{}2
6.  p  :  \mBbbR{}\^{}2
7.  q  :  \mBbbR{}\^{}2
8.  d(a;b)  =  d(a;p)
9.  \mneg{}\mneg{}(\mexists{}w:\mBbbR{}\^{}2.  (c\_w\_d  \mwedge{}  (d(c;w)  =  d(c;p))))
10.  d(c;d)  =  d(c;q)
11.  \mneg{}\mneg{}(\mexists{}w:\mBbbR{}\^{}2.  (a\_w\_b  \mwedge{}  (d(a;w)  =  d(a;q))))
12.  d(a;b)  =  d(a;p)
13.  d(c;d)  =  d(c;q)
\mvdash{}  d(c;p)  \mleq{}  d(c;d)


By

---

Latex:
((StableCases  \mkleeneopen{}\mexists{}w:\mBbbR{}\^{}2.  (c\_w\_d  \mwedge{}  (d(c;w)  =  d(c;p)))\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  ExRepD
  THEN  (FLemma  `rv-be-dist`  [-2]  THENA  Auto)
  THEN  (RWW  "-1  -2"  0  THENA  Auto)
  THEN  nRAdd  \mkleeneopen{}-(d(c;p))\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index