Step
*
4
2
1
1
of Lemma
hp-angle-sum-lt
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. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-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. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
46. xyz < p'j'k'
47. q : Point
48. p'-q-f'
49. xyz ≅a qj'p'
50. ¬out(j' i'k')
⊢ ijk ≅a i'j'q
BY
{ (InstLemma `hp-angle-sum-eq` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜x⌝;⌜y⌝;⌜z⌝;⌜i⌝;⌜j⌝;⌜k⌝;⌜a'⌝;⌜b'⌝;⌜c'⌝;⌜p'⌝;⌜j'⌝;⌜q⌝;⌜i'⌝;⌜j'⌝;⌜q⌝]⋅
THEN Auto
) }
1
.....antecedent.....
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. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-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. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
46. xyz < p'j'k'
47. q : Point
48. p'-q-f'
49. xyz ≅a qj'p'
50. ¬out(j' i'k')
⊢ xyz ≅a p'j'q
2
.....antecedent.....
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. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-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. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
46. xyz < p'j'k'
47. q : Point
48. p'-q-f'
49. xyz ≅a qj'p'
50. ¬out(j' i'k')
⊢ abc + xyz ≅ ijk
3
.....antecedent.....
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. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-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. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
46. xyz < p'j'k'
47. q : Point
48. p'-q-f'
49. xyz ≅a qj'p'
50. ¬out(j' i'k')
⊢ a'b'c' + p'j'q ≅ i'j'q
4
.....antecedent.....
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. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-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. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
46. xyz < p'j'k'
47. q : Point
48. p'-q-f'
49. xyz ≅a qj'p'
50. ¬out(j' i'k')
⊢ i' # j'q
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. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc \mcong{}\msuba{} ijp1
26. kjp1 \mcong{}\msuba{} xyz
27. j\_p2\_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-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. i \# jk
42. i' \# j'k'
43. x \# yz
44. xyz < x'y'z'
45. p' \# j'k'
46. xyz < p'j'k'
47. q : Point
48. p'-q-f'
49. xyz \mcong{}\msuba{} qj'p'
50. \mneg{}out(j' i'k')
\mvdash{} ijk \mcong{}\msuba{} i'j'q
By
Latex:
(InstLemma `hp-angle-sum-eq` [\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{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};
\mkleeneopen{}i'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
THEN Auto
)
Home
Index