---

Step * 2 of Lemma better-r2-straightedge-compass


1. c : ℝ^2
2. d : ℝ^2
3. a : ℝ^2
4. b : {b:ℝ^2| b ≠ a ∧ c_b_d} 
5. ∃q:ℝ^2. (q_a_b ∧ (d(c;d) < d(c;q)))
⊢ ∃u:{u:ℝ^2| cu=cd ∧ a_b_u} 
   (∃v:ℝ^2 [(cv=cd
           ∧ v_b_u
           ∧ (¬((¬a_b_v) ∧ (¬b_v_a) ∧ (¬v_a_b)))
           ∧ (b ≠ d ⇒ v ≠ u)
           ∧ ((¬d ≠ b)
             ⇒ ((v ≠ u ⇒ ((¬u ≠ b) ∨ (¬v ≠ b)))
                ∧ ((¬v ≠ u) ⇒ ((∀a':ℝ^2. ((d(a';b) = d(a;b)) ⇒ a'_b_a ⇒ (d(c;a) = d(c;a')))) ∧ (¬u ≠ b))))))])
BY
{ (ExRepD
   THEN (InstLemma `rv-line-circle-3-ext` [⌜2⌝;⌜c⌝;⌜b⌝;⌜d⌝;⌜q⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN (InstLemma `rv-be-inner-trans` [⌜v⌝;⌜b⌝;⌜a⌝;⌜q⌝]⋅ THENA (Auto THEN BLemma `rv-be-symmetry` THEN Auto))
   THEN (InstLemma `rv-be-inner-trans` [⌜v⌝;⌜b⌝;⌜u⌝;⌜q⌝]⋅ THENA (Auto THEN BLemma `rv-be-symmetry` THEN Auto))) }

1
1. c : ℝ^2
2. d : ℝ^2
3. a : ℝ^2
4. b : {b:ℝ^2| b ≠ a ∧ c_b_d} 
5. q : ℝ^2
6. q_a_b
7. d(c;d) < d(c;q)
8. u : {u:ℝ^2| cd=cu ∧ q_u_b} 
9. v : ℝ^2
10. [%6] : cd=cv
∧ q_b_v
∧ (b ≠ d ⇒ (u ≠ v ∧ u ≠ b ∧ v ≠ b))
∧ (req-vec(2;b;d)
  ⇒ ((u ≠ v ⇒ ((req-vec(2;u;b) ∧ (r0 < b - c⋅q - b)) ∨ (req-vec(2;v;b) ∧ (b - c⋅q - b < r0))))
     ∧ (req-vec(2;u;v) ⇒ ((b - c⋅q - b = r0) ∧ req-vec(2;u;b)))))
11. v_b_a
12. v_b_u
⊢ ∃u:{u:ℝ^2| cu=cd ∧ a_b_u} 
   (∃v:ℝ^2 [(cv=cd
           ∧ v_b_u
           ∧ (¬((¬a_b_v) ∧ (¬b_v_a) ∧ (¬v_a_b)))
           ∧ (b ≠ d ⇒ v ≠ u)
           ∧ ((¬d ≠ b)
             ⇒ ((v ≠ u ⇒ ((¬u ≠ b) ∨ (¬v ≠ b)))
                ∧ ((¬v ≠ u) ⇒ ((∀a':ℝ^2. ((d(a';b) = d(a;b)) ⇒ a'_b_a ⇒ (d(c;a) = d(c;a')))) ∧ (¬u ≠ b))))))])

---

Latex:

---

Latex:

1.  c  :  \mBbbR{}\^{}2
2.  d  :  \mBbbR{}\^{}2
3.  a  :  \mBbbR{}\^{}2
4.  b  :  \{b:\mBbbR{}\^{}2|  b  \mneq{}  a  \mwedge{}  c\_b\_d\} 
5.  \mexists{}q:\mBbbR{}\^{}2.  (q\_a\_b  \mwedge{}  (d(c;d)  <  d(c;q)))
\mvdash{}  \mexists{}u:\{u:\mBbbR{}\^{}2|  cu=cd  \mwedge{}  a\_b\_u\} 
      (\mexists{}v:\mBbbR{}\^{}2  [(cv=cd
                      \mwedge{}  v\_b\_u
                      \mwedge{}  (\mneg{}((\mneg{}a\_b\_v)  \mwedge{}  (\mneg{}b\_v\_a)  \mwedge{}  (\mneg{}v\_a\_b)))
                      \mwedge{}  (b  \mneq{}  d  {}\mRightarrow{}  v  \mneq{}  u)
                      \mwedge{}  ((\mneg{}d  \mneq{}  b)
                          {}\mRightarrow{}  ((v  \mneq{}  u  {}\mRightarrow{}  ((\mneg{}u  \mneq{}  b)  \mvee{}  (\mneg{}v  \mneq{}  b)))
                                \mwedge{}  ((\mneg{}v  \mneq{}  u)
                                    {}\mRightarrow{}  ((\mforall{}a':\mBbbR{}\^{}2.  ((d(a';b)  =  d(a;b))  {}\mRightarrow{}  a'\_b\_a  {}\mRightarrow{}  (d(c;a)  =  d(c;a'))))
                                          \mwedge{}  (\mneg{}u  \mneq{}  b))))))])


By

---

Latex:
(ExRepD
  THEN  (InstLemma  `rv-line-circle-3-ext`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  (InstLemma  `rv-be-inner-trans`  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  BLemma  `rv-be-symmetry`  THEN  Auto)
              )
  THEN  (InstLemma  `rv-be-inner-trans`  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  BLemma  `rv-be-symmetry`  THEN  Auto)
              ))

---

Home Index