---

Step * 2 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. abc < i'j'p
⊢ x'y'z' < xyz
BY
{ (RepeatFor 2 (D -1) THEN RenameVar `p1' (-2)) }

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. 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

---

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.  abc  <  i'j'p
\mvdash{}  x'y'z'  <  xyz


By

---

Latex:
(RepeatFor  2  (D  -1)  THEN  RenameVar  `p1'  (-2))

---

Home Index