---

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


1. c : ℝ^2
2. d : ℝ^2
3. a : ℝ^2
4. b : ℝ^2
5. b ≠ a
6. c_b_d
7. q : ℝ^2
8. q_a_b
9. d(c;d) < d(c;q)
10. u : ℝ^2
11. d(c;d) = d(c;u)
12. q_u_b
13. v : ℝ^2
14. d(c;d) = d(c;v)
15. q_b_v
16. b ≠ d ⇒ (u ≠ v ∧ u ≠ b ∧ v ≠ b)
17. 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))))
18. v_b_a
19. v_b_u
20. d(c;u) = d(c;d)
21. u_b_v
22. ¬((¬a_b_u) ∧ (¬b_u_a) ∧ (¬u_a_b))
23. b ≠ d ⇒ u ≠ v
24. ¬d ≠ b
25. u ≠ v ⇒ ((¬v ≠ b) ∨ (¬u ≠ b))
26. ¬u ≠ v
27. ∀a':ℝ^2. ((d(a';b) = d(a;b)) ⇒ a'_b_a ⇒ (d(c;a) = d(c;a')))
⊢ ¬v ≠ b
BY
{ ((All (RWO  "not-real-vec-sep-iff-eq") THENA Auto)
   THEN (Assert req-vec(2;u;b) BY
               (BackThruSomeHyp THEN RelRST THEN Auto))
   THEN RelRST
   THEN Auto) }

---

Latex:

---

Latex:

1.  c  :  \mBbbR{}\^{}2
2.  d  :  \mBbbR{}\^{}2
3.  a  :  \mBbbR{}\^{}2
4.  b  :  \mBbbR{}\^{}2
5.  b  \mneq{}  a
6.  c\_b\_d
7.  q  :  \mBbbR{}\^{}2
8.  q\_a\_b
9.  d(c;d)  <  d(c;q)
10.  u  :  \mBbbR{}\^{}2
11.  d(c;d)  =  d(c;u)
12.  q\_u\_b
13.  v  :  \mBbbR{}\^{}2
14.  d(c;d)  =  d(c;v)
15.  q\_b\_v
16.  b  \mneq{}  d  {}\mRightarrow{}  (u  \mneq{}  v  \mwedge{}  u  \mneq{}  b  \mwedge{}  v  \mneq{}  b)
17.  req-vec(2;b;d)
{}\mRightarrow{}  ((u  \mneq{}  v  {}\mRightarrow{}  ((req-vec(2;u;b)  \mwedge{}  (r0  <  b  -  c\mcdot{}q  -  b))  \mvee{}  (req-vec(2;v;b)  \mwedge{}  (b  -  c\mcdot{}q  -  b  <  r0))))
      \mwedge{}  (req-vec(2;u;v)  {}\mRightarrow{}  ((b  -  c\mcdot{}q  -  b  =  r0)  \mwedge{}  req-vec(2;u;b))))
18.  v\_b\_a
19.  v\_b\_u
20.  d(c;u)  =  d(c;d)
21.  u\_b\_v
22.  \mneg{}((\mneg{}a\_b\_u)  \mwedge{}  (\mneg{}b\_u\_a)  \mwedge{}  (\mneg{}u\_a\_b))
23.  b  \mneq{}  d  {}\mRightarrow{}  u  \mneq{}  v
24.  \mneg{}d  \mneq{}  b
25.  u  \mneq{}  v  {}\mRightarrow{}  ((\mneg{}v  \mneq{}  b)  \mvee{}  (\mneg{}u  \mneq{}  b))
26.  \mneg{}u  \mneq{}  v
27.  \mforall{}a':\mBbbR{}\^{}2.  ((d(a';b)  =  d(a;b))  {}\mRightarrow{}  a'\_b\_a  {}\mRightarrow{}  (d(c;a)  =  d(c;a')))
\mvdash{}  \mneg{}v  \mneq{}  b


By

---

Latex:
((All  (RWO    "not-real-vec-sep-iff-eq")  THENA  Auto)
  THEN  (Assert  req-vec(2;u;b)  BY
                          (BackThruSomeHyp  THEN  RelRST  THEN  Auto))
  THEN  RelRST
  THEN  Auto)

---

Home Index