Step
*
4
2
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. (p'-q-f' ∧ xyz ≅a qj'p')
48. ¬out(j' i'k')
⊢ ijk < i'j'k'
BY
{ (((Unfold `geo-lt-angle` 0 THEN GenRepD) THEN ExRepD) THEN InstConcl [⌜q⌝;⌜q⌝;⌜d'⌝;⌜f'⌝]⋅ 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. 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
2
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')
51. ijk ≅a i'j'q
52. j'_q_q
53. out(j' i'd')
54. out(j' k'f')
⊢ ¬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. \mexists{}q:Point. (p'-q-f' \mwedge{} xyz \mcong{}\msuba{} qj'p')
48. \mneg{}out(j' i'k')
\mvdash{} ijk < i'j'k'
By
Latex:
(((Unfold `geo-lt-angle` 0 THEN GenRepD) THEN ExRepD) THEN InstConcl [\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index