Step
*
2
1
1
of Lemma
better-r2-straightedge-compass
1. c : ℝ^2
2. d : ℝ^2
3. a : ℝ^2
4. b : {b:ℝ^2| b ≠ a ∧ c_b_d}
5. q : ℝ^2
6. q_a_b
7. d(c;d) < d(c;q)
8. u : {u:ℝ^2| cd=cu ∧ q_u_b}
9. v : ℝ^2
10. [%6] : cd=cv
∧ q_b_v
∧ (b ≠ d ⇒ (u ≠ v ∧ u ≠ b ∧ v ≠ b))
∧ (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)))))
11. v_b_a
12. v_b_u
⊢ ∃v@0:ℝ^2 [(cv@0=cd
∧ v@0_b_v
∧ (¬((¬a_b_v@0) ∧ (¬b_v@0_a) ∧ (¬v@0_a_b)))
∧ (b ≠ d ⇒ v@0 ≠ v)
∧ ((¬d ≠ b)
⇒ ((v@0 ≠ v ⇒ ((¬v ≠ b) ∨ (¬v@0 ≠ b)))
∧ ((¬v@0 ≠ v) ⇒ ((∀a':ℝ^2. ((d(a';b) = d(a;b)) ⇒ a'_b_a ⇒ (d(c;a) = d(c;a')))) ∧ (¬v ≠ b))))))]
BY
{ (UseWitness ⌜u⌝⋅
THEN DSetVars
THEN MemTypeCD
THEN Auto
THEN Try ((BLemma `rv-be-symmetry` THEN Auto))
THEN All (Unfold `rv-congruent`)
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
⊢ ¬((¬a_b_u) ∧ (¬b_u_a) ∧ (¬u_a_b))
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. ¬d ≠ b
25. u ≠ v
⊢ (¬v ≠ b) ∨ (¬u ≠ b)
3
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')
4
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
Latex:
Latex:
1. c : \mBbbR{}\^{}2
2. d : \mBbbR{}\^{}2
3. a : \mBbbR{}\^{}2
4. b : \{b:\mBbbR{}\^{}2| b \mneq{} a \mwedge{} c\_b\_d\}
5. q : \mBbbR{}\^{}2
6. q\_a\_b
7. d(c;d) < d(c;q)
8. u : \{u:\mBbbR{}\^{}2| cd=cu \mwedge{} q\_u\_b\}
9. v : \mBbbR{}\^{}2
10. [\%6] : cd=cv
\mwedge{} q\_b\_v
\mwedge{} (b \mneq{} d {}\mRightarrow{} (u \mneq{} v \mwedge{} u \mneq{} b \mwedge{} v \mneq{} b))
\mwedge{} (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)))))
11. v\_b\_a
12. v\_b\_u
\mvdash{} \mexists{}v@0:\mBbbR{}\^{}2 [(cv@0=cd
\mwedge{} v@0\_b\_v
\mwedge{} (\mneg{}((\mneg{}a\_b\_v@0) \mwedge{} (\mneg{}b\_v@0\_a) \mwedge{} (\mneg{}v@0\_a\_b)))
\mwedge{} (b \mneq{} d {}\mRightarrow{} v@0 \mneq{} v)
\mwedge{} ((\mneg{}d \mneq{} b)
{}\mRightarrow{} ((v@0 \mneq{} v {}\mRightarrow{} ((\mneg{}v \mneq{} b) \mvee{} (\mneg{}v@0 \mneq{} b)))
\mwedge{} ((\mneg{}v@0 \mneq{} v)
{}\mRightarrow{} ((\mforall{}a':\mBbbR{}\^{}2. ((d(a';b) = d(a;b)) {}\mRightarrow{} a'\_b\_a {}\mRightarrow{} (d(c;a) = d(c;a'))))
\mwedge{} (\mneg{}v \mneq{} b))))))]
By
Latex:
(UseWitness \mkleeneopen{}u\mkleeneclose{}\mcdot{}
THEN DSetVars
THEN MemTypeCD
THEN Auto
THEN Try ((BLemma `rv-be-symmetry` THEN Auto))
THEN All (Unfold `rv-congruent`)
THEN Auto)
Home
Index