Step
*
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
⊢ i # jk
BY
{ ((Assert a' # b'c' BY
(ProveLSepFromCong ⌜a'⌝⌜b'⌝⌜c'⌝⌜a⌝⌜b⌝⌜c⌝⋅ THEN EAuto 1))
THEN (Assert d' # j'p BY
((ProveLSepFromCong ⌜d'⌝⌜j'⌝⌜p⌝⌜a'⌝⌜b'⌝⌜c'⌝⋅ THEN Auto)
THEN InstLemma `out-preserves-angle-cong_1` [⌜e⌝;⌜i'⌝;⌜j'⌝;⌜p⌝;⌜a'⌝;⌜b'⌝;⌜c'⌝;⌜d'⌝;⌜p⌝;⌜a'⌝;⌜c'⌝]⋅
THEN EAuto 1))
THEN (Assert x1 # j'z1 BY
((InstLemma `hp-angle-sum-implies-lsep` [⌜e⌝;⌜a'⌝;⌜b'⌝;⌜c'⌝;⌜x'⌝;⌜y'⌝;⌜z'⌝;⌜i'⌝;⌜j'⌝;⌜k'⌝]⋅ THENA Auto)
THEN (ProveLSepFromCong ⌜z1⌝⌜j'⌝⌜x1⌝⌜x'⌝⌜y'⌝⌜z'⌝⋅ THEN EAuto 1)
THEN (InstLemma `out-preserves-angle-cong_1` [⌜e⌝;⌜k'⌝;⌜j'⌝;⌜p⌝;⌜x'⌝;⌜y'⌝;⌜z'⌝;⌜z1⌝;⌜x1⌝;⌜x'⌝;⌜z'⌝]⋅
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
⊢ 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
\mvdash{} i \# jk
By
Latex:
((Assert a' \# b'c' BY
(ProveLSepFromCong \mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}\mkleeneopen{}c'\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{} THEN EAuto 1))
THEN (Assert d' \# j'p BY
((ProveLSepFromCong \mkleeneopen{}d'\mkleeneclose{}\mkleeneopen{}j'\mkleeneclose{}\mkleeneopen{}p\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}\mkleeneopen{}c'\mkleeneclose{}\mcdot{} THEN Auto)
THEN InstLemma `out-preserves-angle-cong\_1` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}i'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};
\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}
THEN EAuto 1))
THEN (Assert x1 \# j'z1 BY
((InstLemma `hp-angle-sum-implies-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}y'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}i'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};
\mkleeneopen{}k'\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN (ProveLSepFromCong \mkleeneopen{}z1\mkleeneclose{}\mkleeneopen{}j'\mkleeneclose{}\mkleeneopen{}x1\mkleeneclose{}\mkleeneopen{}x'\mkleeneclose{}\mkleeneopen{}y'\mkleeneclose{}\mkleeneopen{}z'\mkleeneclose{}\mcdot{} THEN EAuto 1)
THEN (InstLemma `out-preserves-angle-cong\_1` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}k'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}y'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}z1\mkleeneclose{};
\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
THEN Auto
)
THEN D 0
THEN Auto)))
Home
Index