Step
*
2
1
1
of Lemma
unique-angles-in-half-plane
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
10. f : Point
11. acb ≅a fzy
12. x leftof yz ⇐⇒ f leftof yz
13. x leftof zy ⇐⇒ f leftof zy
14. f1 : Point
15. f2 : Point
16. acb ≅a f1zy
17. acb ≅a f2zy
18. x leftof yz ⇒ f1 leftof yz
19. x leftof yz ⇐ f1 leftof yz
20. x leftof zy ⇒ f1 leftof zy
21. x leftof zy ⇐ f1 leftof zy
22. x leftof yz ⇒ f2 leftof yz
23. x leftof yz ⇐ f2 leftof yz
24. x leftof zy ⇒ f2 leftof zy
25. x leftof zy ⇐ f2 leftof zy
26. f2 # z
27. z # y
28. f1 # z
29. z # y
30. a' : Point
31. c' : Point
32. x' : Point
33. z' : Point
34. B(zf2a')
35. B(zyc')
36. B(zf1x')
37. B(zyz')
38. za' ≅ zx'
39. zc' ≅ zz'
40. a'c' ≅ x'z'
41. {z' ≡ c' ∧ ya' ≅ yx'}
⊢ Colinear(z;f1;f2)
BY
{ (D -1 THEN (EliminatePoint (-2) THEN Auto) THEN (Assert x' ≡ a' BY (D 10 THEN Auto))) }
1
.....aux.....
1. e : EuclideanPlane
2. c' : Point
3. a : Point
4. b : Point
5. c : Point
6. x : Point
7. y : Point
8. z : Point
9. a # bc
10. x leftof yz
11. f : Point
12. acb ≅a fzy
13. x leftof yz ⇐ f leftof yz
14. x leftof zy ⇒ f leftof zy
15. x leftof zy ⇐ f leftof zy
16. f1 : Point
17. f2 : Point
18. acb ≅a f1zy
19. acb ≅a f2zy
20. x leftof yz ⇐ f1 leftof yz
21. x leftof zy ⇒ f1 leftof zy
22. x leftof zy ⇐ f1 leftof zy
23. x leftof yz ⇐ f2 leftof yz
24. x leftof zy ⇒ f2 leftof zy
25. x leftof zy ⇐ f2 leftof zy
26. f2 # z
27. z # y
28. f1 # z
29. z # y
30. a' : Point
31. x' : Point
32. z' : Point
33. B(zf2a')
34. B(zyc')
35. B(zf1x')
36. B(zyc')
37. za' ≅ zx'
38. zc' ≅ zc'
39. a'c' ≅ x'c'
40. z' ≡ c'
41. ya' ≅ yx'
42. f2 leftof yz
43. f1 leftof yz
44. f leftof yz
⊢ x' ≡ a'
2
.....aux.....
1. e : EuclideanPlane
2. c' : Point
3. a : Point
4. b : Point
5. c : Point
6. x : Point
7. y : Point
8. z : Point
9. a # bc
10. x leftof zy
11. f : Point
12. acb ≅a fzy
13. x leftof yz ⇒ f leftof yz
14. x leftof yz ⇐ f leftof yz
15. x leftof zy ⇐ f leftof zy
16. f1 : Point
17. f2 : Point
18. acb ≅a f1zy
19. acb ≅a f2zy
20. x leftof yz ⇒ f1 leftof yz
21. x leftof yz ⇐ f1 leftof yz
22. x leftof zy ⇐ f1 leftof zy
23. x leftof yz ⇒ f2 leftof yz
24. x leftof yz ⇐ f2 leftof yz
25. x leftof zy ⇐ f2 leftof zy
26. f2 # z
27. z # y
28. f1 # z
29. z # y
30. a' : Point
31. x' : Point
32. z' : Point
33. B(zf2a')
34. B(zyc')
35. B(zf1x')
36. B(zyc')
37. za' ≅ zx'
38. zc' ≅ zc'
39. a'c' ≅ x'c'
40. z' ≡ c'
41. ya' ≅ yx'
42. f2 leftof zy
43. f1 leftof zy
44. f leftof zy
⊢ x' ≡ a'
3
1. e : EuclideanPlane
2. c' : Point
3. a : Point
4. b : Point
5. c : Point
6. x : Point
7. y : Point
8. z : Point
9. a # bc
10. x # yz
11. f : Point
12. acb ≅a fzy
13. x leftof yz ⇒ f leftof yz
14. x leftof yz ⇐ f leftof yz
15. x leftof zy ⇒ f leftof zy
16. x leftof zy ⇐ f leftof zy
17. f1 : Point
18. f2 : Point
19. acb ≅a f1zy
20. acb ≅a f2zy
21. x leftof yz ⇒ f1 leftof yz
22. x leftof yz ⇐ f1 leftof yz
23. x leftof zy ⇒ f1 leftof zy
24. x leftof zy ⇐ f1 leftof zy
25. x leftof yz ⇒ f2 leftof yz
26. x leftof yz ⇐ f2 leftof yz
27. x leftof zy ⇒ f2 leftof zy
28. x leftof zy ⇐ f2 leftof zy
29. f2 # z
30. z # y
31. f1 # z
32. z # y
33. a' : Point
34. x' : Point
35. z' : Point
36. B(zf2a')
37. B(zyc')
38. B(zf1x')
39. B(zyc')
40. za' ≅ zx'
41. zc' ≅ zc'
42. a'c' ≅ x'c'
43. z' ≡ c'
44. ya' ≅ yx'
45. x' ≡ a'
⊢ Colinear(z;f1;f2)
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a \# bc
9. x \# yz
10. f : Point
11. acb \mcong{}\msuba{} fzy
12. x leftof yz \mLeftarrow{}{}\mRightarrow{} f leftof yz
13. x leftof zy \mLeftarrow{}{}\mRightarrow{} f leftof zy
14. f1 : Point
15. f2 : Point
16. acb \mcong{}\msuba{} f1zy
17. acb \mcong{}\msuba{} f2zy
18. x leftof yz {}\mRightarrow{} f1 leftof yz
19. x leftof yz \mLeftarrow{}{} f1 leftof yz
20. x leftof zy {}\mRightarrow{} f1 leftof zy
21. x leftof zy \mLeftarrow{}{} f1 leftof zy
22. x leftof yz {}\mRightarrow{} f2 leftof yz
23. x leftof yz \mLeftarrow{}{} f2 leftof yz
24. x leftof zy {}\mRightarrow{} f2 leftof zy
25. x leftof zy \mLeftarrow{}{} f2 leftof zy
26. f2 \# z
27. z \# y
28. f1 \# z
29. z \# y
30. a' : Point
31. c' : Point
32. x' : Point
33. z' : Point
34. B(zf2a')
35. B(zyc')
36. B(zf1x')
37. B(zyz')
38. za' \mcong{} zx'
39. zc' \mcong{} zz'
40. a'c' \mcong{} x'z'
41. \{z' \mequiv{} c' \mwedge{} ya' \mcong{} yx'\}
\mvdash{} Colinear(z;f1;f2)
By
Latex:
(D -1 THEN (EliminatePoint (-2) THEN Auto) THEN (Assert x' \mequiv{} a' BY (D 10 THEN Auto)))
Home
Index