---

Step * 1 1 1 1 3 of Lemma geo-lt-angle-trans

.....aux..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. ¬out(e df)
12. p1 : Point
13. p2 : Point
14. x1 : Point
15. z1 : Point
16. abc ≅a dep1
17. B(ep2p1)
18. out(e dx1)
19. out(e fz1)
20. ¬B(dep1)
21. B(x1p2z1)
22. p2 # z1
23. ¬out(y xz)
24. p : Point
25. p' : Point
26. x' : Point
27. z' : Point
28. def ≅a xyp
29. B(yp'p)
30. out(y xx')
31. out(y zz')
32. ¬B(xyp)
33. B(x'p'z')
34. p' # z'
35. a # bc
36. d # ef
37. x # yz
38. x' # yz'
39. out(y pp')
40. x' # p'
41. p' # yx'
42. x2 : Point
43. z2 : Point
44. out(y x2x')
45. out(y z2p')
46. x2y ≅ x1e
47. yz2 ≅ ez1
48. z2x2 ≅ z1x1
49. x2 # yz2
50. z1 # x1e
51. e # p2
52. b' : Point
53. B(z2b'x2)
54. z1p2 ≅ z2b'
55. p2x1 ≅ b'x2
56. Cong3(x2b'z2,x1p2z1)
57. yb' ≅ ep2
58. y # b'
⊢ x2-b'-z2
BY
{ ((D 0 THEN Auto)
   THEN (D -3
         THEN (Assert x1 # p2 BY
                     ((Assert out(e p1p2) BY
                             (InstLemma `geo-between-out` [⌜g⌝;⌜e⌝;⌜p2⌝;⌜p1⌝]⋅ THEN EAuto 1))
                      THEN (InstLemma `out-preserves-angle-cong_1` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜e⌝;⌜p1⌝;⌜a⌝;⌜c⌝;⌜x1⌝;⌜p2⌝]⋅
                            THEN EAuto 1
                            )
                      THEN InstLemma `lsep-cong-angle-implies-sep` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜x1⌝;⌜e⌝;⌜p2⌝]⋅
                      THEN Auto))
         )
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  x  :  Point
9.  y  :  Point
10.  z  :  Point
11.  \mneg{}out(e  df)
12.  p1  :  Point
13.  p2  :  Point
14.  x1  :  Point
15.  z1  :  Point
16.  abc  \mcong{}\msuba{}  dep1
17.  B(ep2p1)
18.  out(e  dx1)
19.  out(e  fz1)
20.  \mneg{}B(dep1)
21.  B(x1p2z1)
22.  p2  \#  z1
23.  \mneg{}out(y  xz)
24.  p  :  Point
25.  p'  :  Point
26.  x'  :  Point
27.  z'  :  Point
28.  def  \mcong{}\msuba{}  xyp
29.  B(yp'p)
30.  out(y  xx')
31.  out(y  zz')
32.  \mneg{}B(xyp)
33.  B(x'p'z')
34.  p'  \#  z'
35.  a  \#  bc
36.  d  \#  ef
37.  x  \#  yz
38.  x'  \#  yz'
39.  out(y  pp')
40.  x'  \#  p'
41.  p'  \#  yx'
42.  x2  :  Point
43.  z2  :  Point
44.  out(y  x2x')
45.  out(y  z2p')
46.  x2y  \mcong{}  x1e
47.  yz2  \mcong{}  ez1
48.  z2x2  \mcong{}  z1x1
49.  x2  \#  yz2
50.  z1  \#  x1e
51.  e  \#  p2
52.  b'  :  Point
53.  B(z2b'x2)
54.  z1p2  \mcong{}  z2b'
55.  p2x1  \mcong{}  b'x2
56.  Cong3(x2b'z2,x1p2z1)
57.  yb'  \mcong{}  ep2
58.  y  \#  b'
\mvdash{}  x2-b'-z2


By

---

Latex:
((D  0  THEN  Auto)
  THEN  (D  -3
              THEN  (Assert  x1  \#  p2  BY
                                      ((Assert  out(e  p1p2)  BY
                                                      (InstLemma  `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{}]\mcdot{}  THEN  EAuto  1))
                                        THEN  (InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};
                                                    \mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{}]\mcdot{}
                                                    THEN  EAuto  1
                                                    )
                                        THEN  InstLemma  `lsep-cong-angle-implies-sep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{}]\mcdot{}
                                        THEN  Auto))
              )
  THEN  Auto)

---

Home Index