Step
*
2
1
1
1
of Lemma
hp-angle-sum-lt3
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. a' # b'c'
21. p3 : Point
22. p4 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp3
26. kjp3 ≅a xyz
27. j_p4_p3
28. out(j id1)
29. out(j kf1)
30. d1-p4-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. ijk ≅a i'j'k'
42. a # bc
43. x # yz
44. i # jk
45. abc < a'b'c'
46. ¬out(j' i'p)
47. p1 : Point
48. p2 : Point
49. x1 : Point
50. z1 : Point
51. abc ≅a i'j'p1
52. j'_p2_p1
53. out(j' i'x1)
54. out(j' pz1)
55. ¬i'_j'_p1
56. x1_p2_z1
57. p2 ≠ z1
58. u : Point
59. j'u ≅ jd1
60. out(j' ui')
61. j ≠ p4
62. j' ≠ p1
63. v : Point
64. j'v ≅ jp4
65. out(j' vp1)
66. j' # i'p1
67. u ≠ v
⊢ x'y'z' < xyz
BY
{ (((gProperProlong ⌜u⌝⌜v⌝`w'⌜p4⌝⌜f1⌝⋅ THENA Auto) THEN ExRepD)
THEN (Assert d1p4 ≅ uv BY
(InstLemma `geo-sas` [⌜e⌝;⌜j⌝;⌜d1⌝;⌜p4⌝;⌜j'⌝;⌜u⌝;⌜v⌝]⋅ THEN Auto))
) }
1
.....aux.....
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. a' # b'c'
21. p3 : Point
22. p4 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp3
26. kjp3 ≅a xyz
27. j_p4_p3
28. out(j id1)
29. out(j kf1)
30. d1-p4-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. ijk ≅a i'j'k'
42. a # bc
43. x # yz
44. i # jk
45. abc < a'b'c'
46. ¬out(j' i'p)
47. p1 : Point
48. p2 : Point
49. x1 : Point
50. z1 : Point
51. abc ≅a i'j'p1
52. j'_p2_p1
53. out(j' i'x1)
54. out(j' pz1)
55. ¬i'_j'_p1
56. x1_p2_z1
57. p2 ≠ z1
58. u : Point
59. j'u ≅ jd1
60. out(j' ui')
61. j ≠ p4
62. j' ≠ p1
63. v : Point
64. j'v ≅ jp4
65. out(j' vp1)
66. j' # i'p1
67. u ≠ v
68. w : Point
69. u-v-w
70. vw ≅ p4f1
⊢ Triangle(j;d1;p4)
2
.....aux.....
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. a' # b'c'
21. p3 : Point
22. p4 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp3
26. kjp3 ≅a xyz
27. j_p4_p3
28. out(j id1)
29. out(j kf1)
30. d1-p4-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. ijk ≅a i'j'k'
42. a # bc
43. x # yz
44. i # jk
45. abc < a'b'c'
46. ¬out(j' i'p)
47. p1 : Point
48. p2 : Point
49. x1 : Point
50. z1 : Point
51. abc ≅a i'j'p1
52. j'_p2_p1
53. out(j' i'x1)
54. out(j' pz1)
55. ¬i'_j'_p1
56. x1_p2_z1
57. p2 ≠ z1
58. u : Point
59. j'u ≅ jd1
60. out(j' ui')
61. j ≠ p4
62. j' ≠ p1
63. v : Point
64. j'v ≅ jp4
65. out(j' vp1)
66. j' # i'p1
67. u ≠ v
68. w : Point
69. u-v-w
70. vw ≅ p4f1
71. Triangle(j;d1;p4)
⊢ Triangle(j';u;v)
3
.....aux.....
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. a' # b'c'
21. p3 : Point
22. p4 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp3
26. kjp3 ≅a xyz
27. j_p4_p3
28. out(j id1)
29. out(j kf1)
30. d1-p4-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. ijk ≅a i'j'k'
42. a # bc
43. x # yz
44. i # jk
45. abc < a'b'c'
46. ¬out(j' i'p)
47. p1 : Point
48. p2 : Point
49. x1 : Point
50. z1 : Point
51. abc ≅a i'j'p1
52. j'_p2_p1
53. out(j' i'x1)
54. out(j' pz1)
55. ¬i'_j'_p1
56. x1_p2_z1
57. p2 ≠ z1
58. u : Point
59. j'u ≅ jd1
60. out(j' ui')
61. j ≠ p4
62. j' ≠ p1
63. v : Point
64. j'v ≅ jp4
65. out(j' vp1)
66. j' # i'p1
67. u ≠ v
68. w : Point
69. u-v-w
70. vw ≅ p4f1
71. jd1 ≅ j'u
72. jp4 ≅ j'v
⊢ d1jp4 ≅a uj'v
4
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. a' # b'c'
21. p3 : Point
22. p4 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp3
26. kjp3 ≅a xyz
27. j_p4_p3
28. out(j id1)
29. out(j kf1)
30. d1-p4-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. ijk ≅a i'j'k'
42. a # bc
43. x # yz
44. i # jk
45. abc < a'b'c'
46. ¬out(j' i'p)
47. p1 : Point
48. p2 : Point
49. x1 : Point
50. z1 : Point
51. abc ≅a i'j'p1
52. j'_p2_p1
53. out(j' i'x1)
54. out(j' pz1)
55. ¬i'_j'_p1
56. x1_p2_z1
57. p2 ≠ z1
58. u : Point
59. j'u ≅ jd1
60. out(j' ui')
61. j ≠ p4
62. j' ≠ p1
63. v : Point
64. j'v ≅ jp4
65. out(j' vp1)
66. j' # i'p1
67. u ≠ v
68. w : Point
69. u-v-w
70. vw ≅ p4f1
71. d1p4 ≅ uv
⊢ x'y'z' < xyz
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. a' \# b'c'
21. p3 : Point
22. p4 : Point
23. d1 : Point
24. f1 : Point
25. abc \mcong{}\msuba{} ijp3
26. kjp3 \mcong{}\msuba{} xyz
27. j\_p4\_p3
28. out(j id1)
29. out(j kf1)
30. d1-p4-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' \mcong{}\msuba{} i'j'p
36. k'j'p \mcong{}\msuba{} x'y'z'
37. j'\_p'\_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. ijk \mcong{}\msuba{} i'j'k'
42. a \# bc
43. x \# yz
44. i \# jk
45. abc < a'b'c'
46. \mneg{}out(j' i'p)
47. p1 : Point
48. p2 : Point
49. x1 : Point
50. z1 : Point
51. abc \mcong{}\msuba{} i'j'p1
52. j'\_p2\_p1
53. out(j' i'x1)
54. out(j' pz1)
55. \mneg{}i'\_j'\_p1
56. x1\_p2\_z1
57. p2 \mneq{} z1
58. u : Point
59. j'u \mcong{} jd1
60. out(j' ui')
61. j \mneq{} p4
62. j' \mneq{} p1
63. v : Point
64. j'v \mcong{} jp4
65. out(j' vp1)
66. j' \# i'p1
67. u \mneq{} v
\mvdash{} x'y'z' < xyz
By
Latex:
(((gProperProlong \mkleeneopen{}u\mkleeneclose{}\mkleeneopen{}v\mkleeneclose{}`w'\mkleeneopen{}p4\mkleeneclose{}\mkleeneopen{}f1\mkleeneclose{}\mcdot{} THENA Auto) THEN ExRepD)
THEN (Assert d1p4 \mcong{} uv BY
(InstLemma `geo-sas` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}p4\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{} THEN Auto))
)
Home
Index