Step * 1 of Lemma hp-angle-sum-eq2


1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. 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. xyz ≅a x'y'z'
22. p1 Point
23. p2 Point
24. d1 Point
25. f1 Point
26. abc ≅a ijp1
27. kjp1 ≅a xyz
28. j_p2_p1
29. out(j id1)
30. out(j kf1)
31. d1-p2-f1
32. Point
33. p' Point
34. d' Point
35. f' Point
36. a'b'c' ≅a i'j'p
37. k'j'p ≅a x'y'z'
38. j'_p'_p
39. out(j' i'd')
40. out(j' k'f')
41. d'-p'-f'
42. bc
43. yz
⊢ ijk ≅a i'j'k'
BY
(((gProperProlong ⌜d1⌝⌜j⌝`A'⌜O⌝⌜X⌝⋅ THENA Auto) THEN (gProperProlong ⌜f1⌝⌜j⌝`B'⌜O⌝⌜X⌝⋅ THENA Auto) THEN ExRepD)
   THEN (gProperProlong ⌜A⌝⌜j⌝`d\'\''⌜j'⌝⌜d'⌝⋅ THENA Auto)
   THEN (gProperProlong ⌜B⌝⌜j⌝`f\'\''⌜j'⌝⌜f'⌝⋅ THENA Auto)
   THEN ExRepD) }

1
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. 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. xyz ≅a x'y'z'
22. p1 Point
23. p2 Point
24. d1 Point
25. f1 Point
26. abc ≅a ijp1
27. kjp1 ≅a xyz
28. j_p2_p1
29. out(j id1)
30. out(j kf1)
31. d1-p2-f1
32. Point
33. p' Point
34. d' Point
35. f' Point
36. a'b'c' ≅a i'j'p
37. k'j'p ≅a x'y'z'
38. j'_p'_p
39. out(j' i'd')
40. out(j' k'f')
41. d'-p'-f'
42. bc
43. yz
44. Point
45. d1-j-A
46. jA ≅ OX
47. Point
48. f1-j-B
49. jB ≅ OX
50. d'' Point
51. A-j-d''
52. jd'' ≅ j'd'
53. f'' Point
54. B-j-f''
55. jf'' ≅ j'f'
⊢ ijk ≅a i'j'k'


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.  xyz  \mcong{}\msuba{}  x'y'z'
22.  p1  :  Point
23.  p2  :  Point
24.  d1  :  Point
25.  f1  :  Point
26.  abc  \mcong{}\msuba{}  ijp1
27.  kjp1  \mcong{}\msuba{}  xyz
28.  j\_p2\_p1
29.  out(j  id1)
30.  out(j  kf1)
31.  d1-p2-f1
32.  p  :  Point
33.  p'  :  Point
34.  d'  :  Point
35.  f'  :  Point
36.  a'b'c'  \mcong{}\msuba{}  i'j'p
37.  k'j'p  \mcong{}\msuba{}  x'y'z'
38.  j'\_p'\_p
39.  out(j'  i'd')
40.  out(j'  k'f')
41.  d'-p'-f'
42.  a  \#  bc
43.  x  \#  yz
\mvdash{}  ijk  \mcong{}\msuba{}  i'j'k'


By


Latex:
(((gProperProlong  \mkleeneopen{}d1\mkleeneclose{}\mkleeneopen{}j\mkleeneclose{}`A'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  (gProperProlong  \mkleeneopen{}f1\mkleeneclose{}\mkleeneopen{}j\mkleeneclose{}`B'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  ExRepD)
  THEN  (gProperProlong  \mkleeneopen{}A\mkleeneclose{}\mkleeneopen{}j\mkleeneclose{}`d\mbackslash{}'\mbackslash{}''\mkleeneopen{}j'\mkleeneclose{}\mkleeneopen{}d'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong  \mkleeneopen{}B\mkleeneclose{}\mkleeneopen{}j\mkleeneclose{}`f\mbackslash{}'\mbackslash{}''\mkleeneopen{}j'\mkleeneclose{}\mkleeneopen{}f'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ExRepD)




Home Index