Step
*
2
1
1
3
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
28. d(a';b) = d(a;b)
29. a'_b_a
⊢ d(c;a) = d(c;a')
BY
{ ((All (RWO "not-real-vec-sep-iff-eq") THENA Auto)
THEN (InstLemma `real-vec-right-angle` [⌜2⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto)
THEN D -1
THEN Thin (-1)
THEN D -1) }
1
.....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
2
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')))
⊢ d(c;a) = d(c;a')
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. a' : \mBbbR{}\^{}2
28. d(a';b) = d(a;b)
29. a'\_b\_a
\mvdash{} d(c;a) = d(c;a')
By
Latex:
((All (RWO "not-real-vec-sep-iff-eq") THENA Auto)
THEN (InstLemma `real-vec-right-angle` [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{} THENA Auto)
THEN D -1
THEN Thin (-1)
THEN D -1)
Home
Index