---

Step * 1 2 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 : ℝ^2
6. ∃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)))
⊢ ↓∃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)))
BY
{ (D 0 THEN RepeatFor 4 (ParallelLast) THEN Try ((RWO "rv-congruent-iff2" 0 THEN Complete (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 : ℝ^2
6. p : ℝ^2
7. q : ℝ^2
8. (¬((d(c;d) < d(c;q)) ∨ (d(c;q) < d(c;d)))) ∧ (d(a;q) < d(a;b))
9. ¬((d(a;b) < d(a;p)) ∨ (d(a;p) < d(a;b)))
10. d(c;p) < d(c;d)
⊢ ↓∃w:ℝ^2. (c_w_d ∧ cw=cp ∧ w ≠ d)

2
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 : ℝ^2
6. p : ℝ^2
7. q : ℝ^2
8. (¬((d(a;b) < d(a;p)) ∨ (d(a;p) < d(a;b)))) ∧ (d(c;p) < d(c;d))
9. ¬((d(c;d) < d(c;q)) ∨ (d(c;q) < d(c;d)))
10. d(a;q) < d(a;b)
⊢ ↓∃w:ℝ^2. (a_w_b ∧ aw=aq ∧ w ≠ b)

---

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  :  \mBbbR{}\^{}2
6.  \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{}  \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)))


By

---

Latex:
(D  0  THEN  RepeatFor  4  (ParallelLast)  THEN  Try  ((RWO  "rv-congruent-iff2"  0  THEN  Complete  (Auto))))

---

Home Index