Step
*
1
1
1
1
1
1
1
1
1
of Lemma
hp-angle-sum-lt2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. abc + xyz ≅ ijk
22. a'b'c' + x'y'z' ≅ i'j'k'
23. i'-j'-k'
24. a # bc
25. x # yz
26. xyz < x'y'z'
27. p : Point
28. p' : Point
29. d' : Point
30. f' : Point
31. a'b'c' ≅a i'j'p
32. k'j'p ≅a x'y'z'
33. j'_p'_p
34. out(j' i'd')
35. out(j' k'f')
36. d'-p'-f'
37. pj'k' ≅a x'y'z'
38. a' # b'c'
39. x' # y'z'
40. p # j'k'
41. ¬out(j' pk')
42. p@0 : Point
43. p1 : Point
44. x1 : Point
45. z1 : Point
46. xyz ≅a pj'p@0
47. j'_p1_p@0
48. out(j' px1)
49. out(j' k'z1)
50. ¬p_j'_p@0
51. x1_p1_z1
52. p1 ≠ z1
53. a' # b'c'
54. d' # j'p
55. x1 # j'z1
56. x1 # j'p@0
57. x1 ≠ p1
⊢ i # jk
BY
{ ((Assert d'_j'_z1 BY
EasyGeometry)
THEN (Assert x1 # z1d' BY
(InstLemma `colinear-lsep` [⌜e⌝;⌜j'⌝;⌜z1⌝;⌜x1⌝;⌜d'⌝]⋅ THEN Auto))
THEN ((InstLemma `lsep-inner-pasch-strict` [⌜e⌝;⌜d'⌝;⌜x1⌝;⌜z1⌝;⌜j'⌝;⌜p1⌝]⋅ THENA Auto)
THENW ((MemTypeCD THEN Auto) THEN D 0 THEN Auto)
)) }
1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. abc + xyz ≅ ijk
22. a'b'c' + x'y'z' ≅ i'j'k'
23. i'-j'-k'
24. a # bc
25. x # yz
26. xyz < x'y'z'
27. p : Point
28. p' : Point
29. d' : Point
30. f' : Point
31. a'b'c' ≅a i'j'p
32. k'j'p ≅a x'y'z'
33. j'_p'_p
34. out(j' i'd')
35. out(j' k'f')
36. d'-p'-f'
37. pj'k' ≅a x'y'z'
38. a' # b'c'
39. x' # y'z'
40. p # j'k'
41. ¬out(j' pk')
42. p@0 : Point
43. p1 : Point
44. x1 : Point
45. z1 : Point
46. xyz ≅a pj'p@0
47. j'_p1_p@0
48. out(j' px1)
49. out(j' k'z1)
50. ¬p_j'_p@0
51. x1_p1_z1
52. p1 ≠ z1
53. a' # b'c'
54. d' # j'p
55. x1 # j'z1
56. x1 # j'p@0
57. x1 ≠ p1
58. d'_j'_z1
59. x1 # z1d'
60. ∃x:Point [(x1-x-j' ∧ d'-x-p1)]
⊢ i # jk
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc \mcong{}\msuba{} a'b'c'
21. abc + xyz \mcong{} ijk
22. a'b'c' + x'y'z' \mcong{} i'j'k'
23. i'-j'-k'
24. a \# bc
25. x \# yz
26. xyz < x'y'z'
27. p : Point
28. p' : Point
29. d' : Point
30. f' : Point
31. a'b'c' \mcong{}\msuba{} i'j'p
32. k'j'p \mcong{}\msuba{} x'y'z'
33. j'\_p'\_p
34. out(j' i'd')
35. out(j' k'f')
36. d'-p'-f'
37. pj'k' \mcong{}\msuba{} x'y'z'
38. a' \# b'c'
39. x' \# y'z'
40. p \# j'k'
41. \mneg{}out(j' pk')
42. p@0 : Point
43. p1 : Point
44. x1 : Point
45. z1 : Point
46. xyz \mcong{}\msuba{} pj'p@0
47. j'\_p1\_p@0
48. out(j' px1)
49. out(j' k'z1)
50. \mneg{}p\_j'\_p@0
51. x1\_p1\_z1
52. p1 \mneq{} z1
53. a' \# b'c'
54. d' \# j'p
55. x1 \# j'z1
56. x1 \# j'p@0
57. x1 \mneq{} p1
\mvdash{} i \# jk
By
Latex:
((Assert d'\_j'\_z1 BY
EasyGeometry)
THEN (Assert x1 \# z1d' BY
(InstLemma `colinear-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}z1\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{}]\mcdot{} THEN Auto))
THEN ((InstLemma `lsep-inner-pasch-strict` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}z1\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{}]\mcdot{} THENA Auto)
THENW ((MemTypeCD THEN Auto) THEN D 0 THEN Auto)
))
Home
Index