---

Step * 2 1 1 1 of Lemma r2-compass-compass


1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. a ≠ c
5. d : ℝ^2
6. ↓∃p,q:ℝ^2. ((ab=ap ∧ (¬¬(∃w:ℝ^2. (c_w_d ∧ cw=cp)))) ∧ cd=cq ∧ (¬¬(∃w:ℝ^2. (a_w_b ∧ aw=aq))))
7. u : ℝ^2
8. ab=au
9. cd=cu
10. v : ℝ^2
11. ab=av
12. cd=cv
13. p : ℝ^2
14. q : ℝ^2
15. d(a;b) = d(a;p)
16. ↓∃w:ℝ^2. (c_w_d ∧ (d(c;w) = d(c;p)) ∧ w ≠ d)
17. d(c;d) = d(c;q)
18. ↓∃w:ℝ^2. (a_w_b ∧ (d(a;w) = d(a;q)) ∧ w ≠ b)
19. d(a;b) = d(a;p)
20. d(c;d) = d(c;q)
⊢ d(c;p) < d(c;d)
BY
{ ((D -5 THEN (Unhide THENA Auto) THEN ExRepD)
   THEN (FLemma `rv-be-dist` [-7] THENA Auto)
   THEN (RWW "-1 -7" 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.  \mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2.  ((ab=ap  \mwedge{}  (\mneg{}\mneg{}(\mexists{}w:\mBbbR{}\^{}2.  (c\_w\_d  \mwedge{}  cw=cp))))  \mwedge{}  cd=cq  \mwedge{}  (\mneg{}\mneg{}(\mexists{}w:\mBbbR{}\^{}2.  (a\_w\_b  \mwedge{}  aw=aq))))
7.  u  :  \mBbbR{}\^{}2
8.  ab=au
9.  cd=cu
10.  v  :  \mBbbR{}\^{}2
11.  ab=av
12.  cd=cv
13.  p  :  \mBbbR{}\^{}2
14.  q  :  \mBbbR{}\^{}2
15.  d(a;b)  =  d(a;p)
16.  \mdownarrow{}\mexists{}w:\mBbbR{}\^{}2.  (c\_w\_d  \mwedge{}  (d(c;w)  =  d(c;p))  \mwedge{}  w  \mneq{}  d)
17.  d(c;d)  =  d(c;q)
18.  \mdownarrow{}\mexists{}w:\mBbbR{}\^{}2.  (a\_w\_b  \mwedge{}  (d(a;w)  =  d(a;q))  \mwedge{}  w  \mneq{}  b)
19.  d(a;b)  =  d(a;p)
20.  d(c;d)  =  d(c;q)
\mvdash{}  d(c;p)  <  d(c;d)


By

---

Latex:
((D  -5  THEN  (Unhide  THENA  Auto)  THEN  ExRepD)
  THEN  (FLemma  `rv-be-dist`  [-7]  THENA  Auto)
  THEN  (RWW  "-1  -7"  0  THENA  Auto)
  THEN  nRAdd  \mkleeneopen{}-(d(c;p))\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index