---

Step * 1 3 5 of Lemma cong-angle-out-exists


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A
28. yA ≅ ba'
29. C : Point
30. r2-y-C
31. yC ≅ bc'
32. a'c' ≅ AC
33. b' : Point
34. A_b'_C
35. a'p ≅ Ab'
36. pc' ≅ b'C
37. A-b'-C
38. Cong3(a'bc',AyC)
39. out(y xA)
40. out(y zC)
41. Ab' ≅ a'p
42. b'C ≅ pc'
⊢ bp ≅ yb'
BY
{ (InstLemma `geo-inner-five-segment` [⌜g⌝;⌜A⌝;⌜b'⌝;⌜C⌝;⌜y⌝;⌜a'⌝;⌜p⌝;⌜c'⌝;⌜b⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  a'  :  Point
9.  c'  :  Point
10.  p  :  Point
11.  abc  \mcong{}\msuba{}  xyz
12.  a  \mneq{}  b
13.  c  \mneq{}  b
14.  p  \mneq{}  b
15.  x  \mneq{}  y
16.  z  \mneq{}  y
17.  out(b  aa')
18.  out(b  cc')
19.  a'-p-c'
20.  r1  :  Point
21.  x-y-r1
22.  yr1  \mcong{}  OX
23.  r2  :  Point
24.  z-y-r2
25.  yr2  \mcong{}  OX
26.  A  :  Point
27.  r1-y-A
28.  yA  \mcong{}  ba'
29.  C  :  Point
30.  r2-y-C
31.  yC  \mcong{}  bc'
32.  a'c'  \mcong{}  AC
33.  b'  :  Point
34.  A\_b'\_C
35.  a'p  \mcong{}  Ab'
36.  pc'  \mcong{}  b'C
37.  A-b'-C
38.  Cong3(a'bc',AyC)
39.  out(y  xA)
40.  out(y  zC)
41.  Ab'  \mcong{}  a'p
42.  b'C  \mcong{}  pc'
\mvdash{}  bp  \mcong{}  yb'


By

---

Latex:
(InstLemma  `geo-inner-five-segment`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index