---

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

.....antecedent..... 
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
⊢ a - b⋅c - b = r0
BY
{ (Assert b - c⋅q - b = r0 BY
         (BackThruSomeHyp THEN RelRST THEN Auto)) }

1
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. b - c⋅q - b = r0
⊢ a - b⋅c - b = r0

---

Latex:

---

Latex:
.....antecedent..... 
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
\mvdash{}  a  -  b\mcdot{}c  -  b  =  r0


By

---

Latex:
(Assert  b  -  c\mcdot{}q  -  b  =  r0  BY
              (BackThruSomeHyp  THEN  RelRST  THEN  Auto))

---

Home Index