---

Step * of Lemma r2-compass-compass-simple

No Annotations
∀a,b:ℝ^2. ∀c:{c:ℝ^2| d(a;a) < d(a;c)} . ∀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
{ (InstLemma `r2-compass-compass-simple1` []⋅ THEN RepeatFor 2 (ParallelLast') THEN Auto) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b:\mBbbR{}\^{}2.  \mforall{}c:\{c:\mBbbR{}\^{}2|  d(a;a)  <  d(a;c)\}  .  \mforall{}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)))\}  .
    (\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:
(InstLemma  `r2-compass-compass-simple1`  []\mcdot{}  THEN  RepeatFor  2  (ParallelLast')  THEN  Auto)

---

Home Index