---

Step * 2 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 ∧ cd=cu
9. v : ℝ^2
10. ab=av ∧ cd=cv
11. (↓∃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))))
⇒ (r2-left(u;c;a) ∧ r2-left(v;a;c))
12. ↓∃p,q:ℝ^2. ((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d))) ∧ cd=cq ∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b)))
⊢ r2-left(v;a;c) ∧ r2-left(u;c;a)
BY
{ (D -2 THENM Auto) }

1
.....antecedent..... 
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 ∧ cd=cu
9. v : ℝ^2
10. ab=av ∧ cd=cv
11. ↓∃p,q:ℝ^2. ((ab=ap ∧ (↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d))) ∧ cd=cq ∧ (↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b)))
⊢ ↓∃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)))

---

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  \mwedge{}  cd=cu
9.  v  :  \mBbbR{}\^{}2
10.  ab=av  \mwedge{}  cd=cv
11.  (\mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2.  (((d(a;b)  =  d(a;p))  \mwedge{}  (d(c;d)  =  d(c;q)))  \mwedge{}  (d(c;p)  <  d(c;d))  \mwedge{}  (d(a;q)  <  d(a;b))))
{}\mRightarrow{}  (r2-left(u;c;a)  \mwedge{}  r2-left(v;a;c))
12.  \mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2
            ((ab=ap  \mwedge{}  (\mdownarrow{}\mexists{}w:\mBbbR{}\^{}2.  (c\_w\_d  \mwedge{}  cw=cp  \mwedge{}  w  \mneq{}  d)))  \mwedge{}  cd=cq  \mwedge{}  (\mdownarrow{}\mexists{}w:\mBbbR{}\^{}2.  (a\_w\_b  \mwedge{}  aw=aq  \mwedge{}  w  \mneq{}  b)))
\mvdash{}  r2-left(v;a;c)  \mwedge{}  r2-left(u;c;a)


By

---

Latex:
(D  -2  THENM  Auto)

---

Home Index