---

Step * 1 of Lemma r2-compass-compass

.....antecedent..... 
1. a : ℝ^2
2. b : ℝ^2
3. c : {c:ℝ^2| a ≠ c} 
4. d : {d:ℝ^2| ↓∃p,q:ℝ^2. ((ab=ap ∧ (¬¬(∃w:ℝ^2. (c_w_d ∧ cw=cp)))) ∧ cd=cq ∧ (¬¬(∃w:ℝ^2. (a_w_b ∧ aw=aq))))} 
⊢ ↓∃p,q:ℝ^2. (((d(a;b) = d(a;p)) ∧ (d(c;d) = d(c;q))) ∧ (d(c;p) ≤ d(c;d)) ∧ (d(a;q) ≤ d(a;b)))
BY
{ (DSetVars THEN RepeatFor 3 (ParallelLast) THEN Unfold `rv-congruent` -1 THEN Auto) }

1
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)

2
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)
14. d(c;p) ≤ d(c;d)
⊢ d(a;q) ≤ d(a;b)

---

Latex:

---

Latex:
.....antecedent..... 
1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  c  :  \{c:\mBbbR{}\^{}2|  a  \mneq{}  c\} 
4.  d  :  \{d:\mBbbR{}\^{}2| 
                \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))))\} 
\mvdash{}  \mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2.  (((d(a;b)  =  d(a;p))  \mwedge{}  (d(c;d)  =  d(c;q)))  \mwedge{}  (d(c;p)  \mleq{}  d(c;d))  \mwedge{}  (d(a;q)  \mleq{}  d(a;b)))


By

---

Latex:
(DSetVars  THEN  RepeatFor  3  (ParallelLast)  THEN  Unfold  `rv-congruent`  -1  THEN  Auto)

---

Home Index