---

Step * of Lemma r2-compass-compass

∀a,b:ℝ^2. ∀c:{c:ℝ^2| a ≠ c} . ∀d:{d:ℝ^2| 
                                 ↓∃p,q:ℝ^2
                                   ((ab=ap ∧ (¬¬(∃w:ℝ^2. (c_w_d ∧ cw=cp)))) ∧ cd=cq ∧ (¬¬(∃w:ℝ^2. (a_w_b ∧ aw=aq))))} .
  ∃u:{u:ℝ^2| ab=au ∧ cd=cu} 
   (∃v:{ℝ^2| ((ab=av ∧ cd=cv)
             ∧ ((↓∃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(u;a;c) ∧ r2-left(v;c;a))))})
BY
{ (Auto THEN (InstLemma `rv-compass-compass-lemma` [⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅ THENA Auto)) }

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

2
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))))} 
5. ∃u,v:{p:ℝ^2| ab=ap ∧ cd=cp} 
    ((↓∃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)))
⊢ ∃u:{u:ℝ^2| ab=au ∧ cd=cu} 
   (∃v:{ℝ^2| ((ab=av ∧ cd=cv)
             ∧ ((↓∃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(u;a;c) ∧ r2-left(v;c;a))))})

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}\^{}2.  \mforall{}c:\{c:\mBbbR{}\^{}2|  a  \mneq{}  c\}  .  \mforall{}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))))\}  .
    \mexists{}u:\{u:\mBbbR{}\^{}2|  ab=au  \mwedge{}  cd=cu\} 
      (\mexists{}v:\{\mBbbR{}\^{}2|  ((ab=av  \mwedge{}  cd=cv)
                          \mwedge{}  ((\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))))
                              {}\mRightarrow{}  (r2-left(u;a;c)  \mwedge{}  r2-left(v;c;a))))\})


By

---

Latex:
(Auto  THEN  (InstLemma  `rv-compass-compass-lemma`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index