Step
*
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
⊢ i # jk
BY
{ ((Assert x1 # j'p@0 BY
((ProveLSepFromCong ⌜p⌝⌜j'⌝⌜p@0⌝⌜x⌝⌜y⌝⌜z⌝⋅ THEN EAuto 1)
THEN InstLemma `colinear-lsep` [⌜e⌝;⌜p⌝;⌜j'⌝;⌜p@0⌝;⌜x1⌝]⋅
THEN Auto))
THEN (Assert x1 ≠ p1 BY
(InstLemma `lsep-iff-all-sep` [⌜e⌝;⌜x1⌝;⌜j'⌝;⌜p@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
⊢ 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
\mvdash{} i \# jk
By
Latex:
((Assert x1 \# j'p@0 BY
((ProveLSepFromCong \mkleeneopen{}p\mkleeneclose{}\mkleeneopen{}j'\mkleeneclose{}\mkleeneopen{}p@0\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}z\mkleeneclose{}\mcdot{} THEN EAuto 1)
THEN InstLemma `colinear-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p@0\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}
THEN Auto))
THEN (Assert x1 \mneq{} p1 BY
(InstLemma `lsep-iff-all-sep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p@0\mkleeneclose{}]\mcdot{} THEN Auto))
)
Home
Index