---

Step * 1 1 1 1 4 2 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. p1 : Point
12. p2 : Point
13. x1 : Point
14. z1 : Point
15. abc ≅a dep1
16. B(ep2p1)
17. out(e dx1)
18. out(e fz1)
19. ¬B(dep1)
20. B(x1p2z1)
21. p2 # z1
22. p : Point
23. p' : Point
24. x' : Point
25. z' : Point
26. def ≅a xyp
27. B(yp'p)
28. out(y xx')
29. out(y zz')
30. ¬B(xyp)
31. B(x'p'z')
32. p' # z'
33. a # bc
34. d # ef
35. x # yz
36. x' # yz'
37. out(y pp')
38. x' # p'
39. p' # yx'
40. x2 : Point
41. z2 : Point
42. out(y x2x')
43. out(y z2p')
44. Cong3(x2yz2,x1ez1)
45. x2 # yz2
46. z1 # x1e
47. e # p2
48. ∃p'':Point. ((Cong3(x2p''z2,x1p2z1) ∧ yp'' ≅ ep2 ∧ y # p'') ∧ x2-p''-z2)
⊢ ∃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
{ ((ExRepD THEN (InstLemma `geo-out-interior-point-exists` [⌜g⌝;⌜x2⌝;⌜y⌝;⌜z2⌝;⌜x'⌝;⌜p'⌝;⌜p''⌝]⋅ THENA Auto) THEN ExRepD)
   THEN RenameVar `P' (-5)
   ) }

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. p1 : Point
12. p2 : Point
13. x1 : Point
14. z1 : Point
15. abc ≅a dep1
16. B(ep2p1)
17. out(e dx1)
18. out(e fz1)
19. ¬B(dep1)
20. B(x1p2z1)
21. p2 # z1
22. p : Point
23. p' : Point
24. x' : Point
25. z' : Point
26. def ≅a xyp
27. B(yp'p)
28. out(y xx')
29. out(y zz')
30. ¬B(xyp)
31. B(x'p'z')
32. p' # z'
33. a # bc
34. d # ef
35. x # yz
36. x' # yz'
37. out(y pp')
38. x' # p'
39. p' # yx'
40. x2 : Point
41. z2 : Point
42. out(y x2x')
43. out(y z2p')
44. Cong3(x2yz2,x1ez1)
45. x2 # yz2
46. z1 # x1e
47. e # p2
48. p'' : Point
49. Cong3(x2p''z2,x1p2z1)
50. yp'' ≅ ep2
51. y # p''
52. x2-p''-z2
53. P : Point
54. x'-P-p'
55. out(y p''P)
56. x2yp'' ≅a x'yP
57. z2yp'' ≅a p'yP
⊢ ∃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.  p1  :  Point
12.  p2  :  Point
13.  x1  :  Point
14.  z1  :  Point
15.  abc  \mcong{}\msuba{}  dep1
16.  B(ep2p1)
17.  out(e  dx1)
18.  out(e  fz1)
19.  \mneg{}B(dep1)
20.  B(x1p2z1)
21.  p2  \#  z1
22.  p  :  Point
23.  p'  :  Point
24.  x'  :  Point
25.  z'  :  Point
26.  def  \mcong{}\msuba{}  xyp
27.  B(yp'p)
28.  out(y  xx')
29.  out(y  zz')
30.  \mneg{}B(xyp)
31.  B(x'p'z')
32.  p'  \#  z'
33.  a  \#  bc
34.  d  \#  ef
35.  x  \#  yz
36.  x'  \#  yz'
37.  out(y  pp')
38.  x'  \#  p'
39.  p'  \#  yx'
40.  x2  :  Point
41.  z2  :  Point
42.  out(y  x2x')
43.  out(y  z2p')
44.  Cong3(x2yz2,x1ez1)
45.  x2  \#  yz2
46.  z1  \#  x1e
47.  e  \#  p2
48.  \mexists{}p'':Point.  ((Cong3(x2p''z2,x1p2z1)  \mwedge{}  yp''  \mcong{}  ep2  \mwedge{}  y  \#  p'')  \mwedge{}  x2-p''-z2)
\mvdash{}  \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:
((ExRepD
    THEN  (InstLemma  `geo-out-interior-point-exists`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z2\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}p''\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  ExRepD)
  THEN  RenameVar  `P'  (-5)
  )

---

Home Index