Step
*
2
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. abc + xyz ≅ ijk
22. p : 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. a # bc
34. x # yz
35. i # 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 j # d1p4 BY
                            Auto)
                THEN Auto))
   THEN (Assert j' ≠ p1 BY
               Auto)
   THEN (DrawAlong ⌜j'⌝⌜p1⌝⌜j⌝⌜p4⌝`v'⋅ THENA 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. 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)
⊢ 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