---

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


1. a : ℝ^2
2. b : ℝ^2
3. ∀c:{c:ℝ^2| a ≠ c} . ∀d:{d:ℝ^2| 
                          ↓∃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)))} .
     (∃u:ℝ^2 [(ab=au ∧ cd=cu ∧ r2-left(u;a;c))])
4. c : {c:ℝ^2| d(a;a) < d(a;c)} 
5. d : {d:ℝ^2| 
        ↓∃p,q:ℝ^2
          (((¬((d(a;b) < d(a;p)) ∨ (d(a;p) < d(a;b)))) ∧ (d(c;p) < d(c;d)))
          ∧ (¬((d(c;d) < d(c;q)) ∨ (d(c;q) < d(c;d))))
          ∧ (d(a;q) < d(a;b)))} 
⊢ ∃u:ℝ^2 [((¬((d(a;b) < d(a;u)) ∨ (d(a;u) < d(a;b)))) ∧ (¬((d(c;d) < d(c;u)) ∨ (d(c;u) < d(c;d)))) ∧ r2-left(u;a;c))]
BY
{ InstHyp [⌜c⌝;⌜d⌝] 3⋅ }

1
.....wf..... 
1. a : ℝ^2
2. b : ℝ^2
3. ∀c:{c:ℝ^2| a ≠ c} . ∀d:{d:ℝ^2| 
                          ↓∃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)))} .
     (∃u:ℝ^2 [(ab=au ∧ cd=cu ∧ r2-left(u;a;c))])
4. c : {c:ℝ^2| d(a;a) < d(a;c)} 
5. d : {d:ℝ^2| 
        ↓∃p,q:ℝ^2
          (((¬((d(a;b) < d(a;p)) ∨ (d(a;p) < d(a;b)))) ∧ (d(c;p) < d(c;d)))
          ∧ (¬((d(c;d) < d(c;q)) ∨ (d(c;q) < d(c;d))))
          ∧ (d(a;q) < d(a;b)))} 
⊢ c ∈ {c:ℝ^2| a ≠ c} 

2
.....wf..... 
1. a : ℝ^2
2. b : ℝ^2
3. ∀c:{c:ℝ^2| a ≠ c} . ∀d:{d:ℝ^2| 
                          ↓∃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)))} .
     (∃u:ℝ^2 [(ab=au ∧ cd=cu ∧ r2-left(u;a;c))])
4. c : {c:ℝ^2| d(a;a) < d(a;c)} 
5. d : {d:ℝ^2| 
        ↓∃p,q:ℝ^2
          (((¬((d(a;b) < d(a;p)) ∨ (d(a;p) < d(a;b)))) ∧ (d(c;p) < d(c;d)))
          ∧ (¬((d(c;d) < d(c;q)) ∨ (d(c;q) < d(c;d))))
          ∧ (d(a;q) < d(a;b)))} 
⊢ d ∈ {d:ℝ^2| ↓∃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)))} 

3
1. a : ℝ^2
2. b : ℝ^2
3. ∀c:{c:ℝ^2| a ≠ c} . ∀d:{d:ℝ^2| 
                          ↓∃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)))} .
     (∃u:ℝ^2 [(ab=au ∧ cd=cu ∧ r2-left(u;a;c))])
4. c : {c:ℝ^2| d(a;a) < d(a;c)} 
5. d : {d:ℝ^2| 
        ↓∃p,q:ℝ^2
          (((¬((d(a;b) < d(a;p)) ∨ (d(a;p) < d(a;b)))) ∧ (d(c;p) < d(c;d)))
          ∧ (¬((d(c;d) < d(c;q)) ∨ (d(c;q) < d(c;d))))
          ∧ (d(a;q) < d(a;b)))} 
6. ∃u:ℝ^2 [(ab=au ∧ cd=cu ∧ r2-left(u;a;c))]
⊢ ∃u:ℝ^2 [((¬((d(a;b) < d(a;u)) ∨ (d(a;u) < d(a;b)))) ∧ (¬((d(c;d) < d(c;u)) ∨ (d(c;u) < d(c;d)))) ∧ r2-left(u;a;c))]

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  \mforall{}c:\{c:\mBbbR{}\^{}2|  a  \mneq{}  c\}  .  \mforall{}d:\{d:\mBbbR{}\^{}2| 
                                                    \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)))\}  .
          (\mexists{}u:\mBbbR{}\^{}2  [(ab=au  \mwedge{}  cd=cu  \mwedge{}  r2-left(u;a;c))])
4.  c  :  \{c:\mBbbR{}\^{}2|  d(a;a)  <  d(a;c)\} 
5.  d  :  \{d:\mBbbR{}\^{}2| 
                \mdownarrow{}\mexists{}p,q:\mBbbR{}\^{}2
                    (((\mneg{}((d(a;b)  <  d(a;p))  \mvee{}  (d(a;p)  <  d(a;b))))  \mwedge{}  (d(c;p)  <  d(c;d)))
                    \mwedge{}  (\mneg{}((d(c;d)  <  d(c;q))  \mvee{}  (d(c;q)  <  d(c;d))))
                    \mwedge{}  (d(a;q)  <  d(a;b)))\} 
\mvdash{}  \mexists{}u:\mBbbR{}\^{}2  [((\mneg{}((d(a;b)  <  d(a;u))  \mvee{}  (d(a;u)  <  d(a;b))))
                  \mwedge{}  (\mneg{}((d(c;d)  <  d(c;u))  \mvee{}  (d(c;u)  <  d(c;d))))
                  \mwedge{}  r2-left(u;a;c))]


By

---

Latex:
InstHyp  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]  3\mcdot{}

---

Home Index