---

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


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
⊢ (¬out(y xz))
∧ (∃p,p',x',z':Point. (abc ≅a xyp ∧ B(yp'p) ∧ (out(y xx') ∧ out(y zz')) ∧ (¬B(xyp)) ∧ B(x'p'z') ∧ p' # z'))
BY
{ ((Assert x' # yz' BY
          (InstLemma `out-preserves-lsep` [⌜g⌝;⌜y⌝;⌜x⌝;⌜z⌝;⌜x'⌝;⌜z'⌝]⋅ THEN EAuto 1))
   THEN (Assert out(y pp') BY
               ((InstLemma `geo-between-out` [⌜g⌝;⌜y⌝;⌜p'⌝;⌜p⌝]⋅ THEN Auto)
                THEN InstLemma `colinear-lsep` [⌜g⌝;⌜x'⌝;⌜z'⌝;⌜y⌝;⌜p'⌝]⋅
                THEN EAuto 1))
   THEN (Assert x' # p' BY
               ((InstLemma `out-preserves-angle-cong_1` [⌜g⌝;⌜d⌝;⌜e⌝;⌜f⌝;⌜x⌝;⌜y⌝;⌜p⌝;⌜d⌝;⌜f⌝;⌜x'⌝;⌜p'⌝]⋅ THEN EAuto 1)
                THEN InstLemma `lsep-cong-angle-implies-sep` [⌜g⌝;⌜d⌝;⌜e⌝;⌜f⌝;⌜x'⌝;⌜y⌝;⌜p'⌝]⋅
                THEN Auto))
   THEN (Assert p' # yx' BY
               (InstLemma `colinear-lsep` [⌜g⌝;⌜z'⌝;⌜x'⌝;⌜y⌝;⌜p'⌝]⋅ THEN Auto))) }

1
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'
⊢ (¬out(y xz))
∧ (∃p,p',x',z':Point. (abc ≅a xyp ∧ B(yp'p) ∧ (out(y xx') ∧ out(y zz')) ∧ (¬B(xyp)) ∧ B(x'p'z') ∧ p' # z'))

---

Latex:

---

Latex:

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
\mvdash{}  (\mneg{}out(y  xz))
\mwedge{}  (\mexists{}p,p',x',z':Point
        (abc  \mcong{}\msuba{}  xyp  \mwedge{}  B(yp'p)  \mwedge{}  (out(y  xx')  \mwedge{}  out(y  zz'))  \mwedge{}  (\mneg{}B(xyp))  \mwedge{}  B(x'p'z')  \mwedge{}  p'  \#  z'))


By

---

Latex:
((Assert  x'  \#  yz'  BY
                (InstLemma  `out-preserves-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}  THEN  EAuto  1))
  THEN  (Assert  out(y  pp')  BY
                          ((InstLemma  `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THEN  InstLemma  `colinear-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{}
                            THEN  EAuto  1))
  THEN  (Assert  x'  \#  p'  BY
                          ((InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}
                              ]\mcdot{}
                              THEN  EAuto  1
                              )
                            THEN  InstLemma  `lsep-cong-angle-implies-sep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  (Assert  p'  \#  yx'  BY
                          (InstLemma  `colinear-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{}  THEN  Auto)))

---

Home Index