---

Step * 2 1 1 3 2 2 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. req-vec(2;d;b)
25. u ≠ v ⇒ (req-vec(2;v;b) ∨ req-vec(2;u;b))
26. req-vec(2;u;v)
27. a' : ℝ^2
28. d(a';b) = d(a;b)
29. a'_b_a
30. ∀x':ℝ^2. ((d(x';b) = d(a;b)) ⇒ real-vec-be(2;a;b;x') ⇒ (d(c;a) = d(c;x')))
31. ¬real-vec-be(2;a;b;a')
32. ¬a' ≠ b
⊢ False
BY
{ (((RWO  "not-real-vec-sep-iff-eq" (-1)) THENA Auto)
   THEN D -2
   THEN (D 0 With ⌜r0⌝  THEN Auto)
   THEN RepeatFor 2 (ParallelOp -2)
   THEN RepUR ``real-vec-add real-vec-mul`` 0
   THEN Auto
   THEN nRNorm 0
   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.  req-vec(2;d;b)
25.  u  \mneq{}  v  {}\mRightarrow{}  (req-vec(2;v;b)  \mvee{}  req-vec(2;u;b))
26.  req-vec(2;u;v)
27.  a'  :  \mBbbR{}\^{}2
28.  d(a';b)  =  d(a;b)
29.  a'\_b\_a
30.  \mforall{}x':\mBbbR{}\^{}2.  ((d(x';b)  =  d(a;b))  {}\mRightarrow{}  real-vec-be(2;a;b;x')  {}\mRightarrow{}  (d(c;a)  =  d(c;x')))
31.  \mneg{}real-vec-be(2;a;b;a')
32.  \mneg{}a'  \mneq{}  b
\mvdash{}  False


By

---

Latex:
(((RWO    "not-real-vec-sep-iff-eq"  (-1))  THENA  Auto)
  THEN  D  -2
  THEN  (D  0  With  \mkleeneopen{}r0\mkleeneclose{}    THEN  Auto)
  THEN  RepeatFor  2  (ParallelOp  -2)
  THEN  RepUR  ``real-vec-add  real-vec-mul``  0
  THEN  Auto
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index