Step * 2 1 of Lemma hp-angle-sum-lt3


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. a' b'c'
21. abc xyz ≅ ijk
22. Point
23. p' Point
24. d' Point
25. f' Point
26. a'b'c' ≅a i'j'p
27. k'j'p ≅a x'y'z'
28. j'_p'_p
29. out(j' i'd')
30. out(j' k'f')
31. d'-p'-f'
32. ijk ≅a i'j'k'
33. bc
34. yz
35. jk
36. abc < a'b'c'
37. ¬out(j' i'p)
38. p1 Point
39. ∃p',x',z':Point. (abc ≅a i'j'p1 ∧ j'_p'_p1 ∧ (out(j' i'x') ∧ out(j' pz')) ∧ i'_j'_p1) ∧ x'_p'_z' ∧ p' ≠ z')
⊢ x'y'z' < xyz
BY
(Unfold `hp-angle-sum` 21
   THEN ExRepD
   THEN (DrawAlong ⌜j'⌝⌜i'⌝⌜j⌝⌜d1⌝`u'⋅ THENA Auto)
   THEN (Assert j ≠ p4 BY
               ((InstLemma `out-preserves-lsep` [⌜e⌝;⌜j⌝;⌜i⌝;⌜k⌝;⌜d1⌝;⌜f1⌝]⋅ THENA EAuto 1)
                THEN (Assert d1p4 BY
                            Auto)
                THEN Auto))
   THEN (Assert j' ≠ p1 BY
               Auto)
   THEN (DrawAlong ⌜j'⌝⌜p1⌝⌜j⌝⌜p4⌝`v'⋅ THENA Auto)) }

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. 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. 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. bc
43. yz
44. 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. Point
59. j'u ≅ jd1
60. out(j' ui')
61. j ≠ p4
62. j' ≠ p1
63. Point
64. j'v ≅ jp4
65. out(j' vp1)
⊢ 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.  abc  +  xyz  \mcong{}  ijk
22.  p  :  Point
23.  p'  :  Point
24.  d'  :  Point
25.  f'  :  Point
26.  a'b'c'  \mcong{}\msuba{}  i'j'p
27.  k'j'p  \mcong{}\msuba{}  x'y'z'
28.  j'\_p'\_p
29.  out(j'  i'd')
30.  out(j'  k'f')
31.  d'-p'-f'
32.  ijk  \mcong{}\msuba{}  i'j'k'
33.  a  \#  bc
34.  x  \#  yz
35.  i  \#  jk
36.  abc  <  a'b'c'
37.  \mneg{}out(j'  i'p)
38.  p1  :  Point
39.  \mexists{}p',x',z':Point
          (abc  \mcong{}\msuba{}  i'j'p1  \mwedge{}  j'\_p'\_p1  \mwedge{}  (out(j'  i'x')  \mwedge{}  out(j'  pz'))  \mwedge{}  (\mneg{}i'\_j'\_p1)  \mwedge{}  x'\_p'\_z'  \mwedge{}  p'  \mneq{}  z')
\mvdash{}  x'y'z'  <  xyz


By


Latex:
(Unfold  `hp-angle-sum`  21
  THEN  ExRepD
  THEN  (DrawAlong  \mkleeneopen{}j'\mkleeneclose{}\mkleeneopen{}i'\mkleeneclose{}\mkleeneopen{}j\mkleeneclose{}\mkleeneopen{}d1\mkleeneclose{}`u'\mcdot{}  THENA  Auto)
  THEN  (Assert  j  \mneq{}  p4  BY
                          ((InstLemma  `out-preserves-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}f1\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
                            THEN  (Assert  j  \#  d1p4  BY
                                                    Auto)
                            THEN  Auto))
  THEN  (Assert  j'  \mneq{}  p1  BY
                          Auto)
  THEN  (DrawAlong  \mkleeneopen{}j'\mkleeneclose{}\mkleeneopen{}p1\mkleeneclose{}\mkleeneopen{}j\mkleeneclose{}\mkleeneopen{}p4\mkleeneclose{}`v'\mcdot{}  THENA  Auto))




Home Index