---

Step * of Lemma r2-straightedge-compass

∀c,d,a:ℝ^2. ∀b:{b:ℝ^2| b ≠ a ∧ c_b_d} .
  ∃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 ∧ u ≠ b ∧ v ≠ b)))])
BY
{ (Auto THEN Assert ⌜∃q:ℝ^2. (q_a_b ∧ (d(c;d) < d(c;q)))⌝⋅) }

1
.....assertion..... 
1. c : ℝ^2
2. d : ℝ^2
3. a : ℝ^2
4. b : {b:ℝ^2| b ≠ a ∧ c_b_d} 
⊢ ∃q:ℝ^2. (q_a_b ∧ (d(c;d) < d(c;q)))

2
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 ∧ u ≠ b ∧ v ≠ b)))])

---

Latex:

---

Latex:
\mforall{}c,d,a:\mBbbR{}\^{}2.  \mforall{}b:\{b:\mBbbR{}\^{}2|  b  \mneq{}  a  \mwedge{}  c\_b\_d\}  .
    \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{}  u  \mneq{}  b  \mwedge{}  v  \mneq{}  b)))])


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mexists{}q:\mBbbR{}\^{}2.  (q\_a\_b  \mwedge{}  (d(c;d)  <  d(c;q)))\mkleeneclose{}\mcdot{})

---

Home Index