---

Step * of Lemma better-r2-straightedge-compass

No Annotations
∀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)
           ∧ ((¬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
{ (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)
           ∧ ((¬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:
No  Annotations
\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{}  ((\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:
(Auto  THEN  Assert  \mkleeneopen{}\mexists{}q:\mBbbR{}\^{}2.  (q\_a\_b  \mwedge{}  (d(c;d)  <  d(c;q)))\mkleeneclose{}\mcdot{})

---

Home Index