---

Step * 1 1 1 of Lemma opp-side_half-plane-angle-congruence


1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. a leftof bp
11. c leftof pb
12. a' leftof b'p'
13. c' leftof p'b'
14. abp ≅a a'b'p'
15. pbc ≅a p'b'c'
16. a # b
17. b # p
18. a' # b'
19. b' # p'
20. a'@0 : Point
21. c1 : Point
22. x1 : Point
23. z1 : Point
24. B(baa'@0)
25. B(bpc1)
26. B(b'a'x1)
27. B(b'p'z1)
28. ba'@0 ≅ b'x1
29. bc1 ≅ b'z1
30. a'@0c1 ≅ x1z1
31. p # b
32. b # c
33. p' # b'
34. b' # c'
35. a1 : Point
36. c'@0 : Point
37. x' : Point
38. z' : Point
39. B(bpa1)
40. B(bcc'@0)
41. B(b'p'x')
42. B(b'c'z')
43. ba1 ≅ b'x'
44. bc'@0 ≅ b'z'
45. a1c'@0 ≅ x'z'
46. B(baa'@0)
47. B(bcc'@0)
48. B(b'a'x1)
49. B(b'c'z')
50. ba'@0 ≅ b'x1
51. bc'@0 ≅ b'z'
52. a'@0 leftof bp
53. c'@0 leftof pb
54. x1 leftof b'p'
55. z' leftof p'b'
56. a'@0ba1 ≅a x1b'x'
57. a1bc'@0 ≅a x'b'z'
⊢ a'@0c'@0 ≅ x1z'
BY
{ (Assert x' # z' BY
         ((InstLemma `lsep-iff-all-sep` [⌜e⌝;⌜z'⌝;⌜p'⌝;⌜b'⌝]⋅ THENA Auto)
          THEN ((D -1 THEN D -2) THENA (Unfold `geo-lsep` 0 THEN Auto))
          THEN D -1
          THEN InstHyp [⌜x'⌝] (-2)⋅
          THEN Auto)) }

1
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. a leftof bp
11. c leftof pb
12. a' leftof b'p'
13. c' leftof p'b'
14. abp ≅a a'b'p'
15. pbc ≅a p'b'c'
16. a # b
17. b # p
18. a' # b'
19. b' # p'
20. a'@0 : Point
21. c1 : Point
22. x1 : Point
23. z1 : Point
24. B(baa'@0)
25. B(bpc1)
26. B(b'a'x1)
27. B(b'p'z1)
28. ba'@0 ≅ b'x1
29. bc1 ≅ b'z1
30. a'@0c1 ≅ x1z1
31. p # b
32. b # c
33. p' # b'
34. b' # c'
35. a1 : Point
36. c'@0 : Point
37. x' : Point
38. z' : Point
39. B(bpa1)
40. B(bcc'@0)
41. B(b'p'x')
42. B(b'c'z')
43. ba1 ≅ b'x'
44. bc'@0 ≅ b'z'
45. a1c'@0 ≅ x'z'
46. B(baa'@0)
47. B(bcc'@0)
48. B(b'a'x1)
49. B(b'c'z')
50. ba'@0 ≅ b'x1
51. bc'@0 ≅ b'z'
52. a'@0 leftof bp
53. c'@0 leftof pb
54. x1 leftof b'p'
55. z' leftof p'b'
56. a'@0ba1 ≅a x1b'x'
57. a1bc'@0 ≅a x'b'z'
58. x' # z'
⊢ a'@0c'@0 ≅ x1z'

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  b  :  Point
3.  p  :  Point
4.  b'  :  Point
5.  p'  :  Point
6.  a  :  Point
7.  c  :  Point
8.  a'  :  Point
9.  c'  :  Point
10.  a  leftof  bp
11.  c  leftof  pb
12.  a'  leftof  b'p'
13.  c'  leftof  p'b'
14.  abp  \mcong{}\msuba{}  a'b'p'
15.  pbc  \mcong{}\msuba{}  p'b'c'
16.  a  \#  b
17.  b  \#  p
18.  a'  \#  b'
19.  b'  \#  p'
20.  a'@0  :  Point
21.  c1  :  Point
22.  x1  :  Point
23.  z1  :  Point
24.  B(baa'@0)
25.  B(bpc1)
26.  B(b'a'x1)
27.  B(b'p'z1)
28.  ba'@0  \mcong{}  b'x1
29.  bc1  \mcong{}  b'z1
30.  a'@0c1  \mcong{}  x1z1
31.  p  \#  b
32.  b  \#  c
33.  p'  \#  b'
34.  b'  \#  c'
35.  a1  :  Point
36.  c'@0  :  Point
37.  x'  :  Point
38.  z'  :  Point
39.  B(bpa1)
40.  B(bcc'@0)
41.  B(b'p'x')
42.  B(b'c'z')
43.  ba1  \mcong{}  b'x'
44.  bc'@0  \mcong{}  b'z'
45.  a1c'@0  \mcong{}  x'z'
46.  B(baa'@0)
47.  B(bcc'@0)
48.  B(b'a'x1)
49.  B(b'c'z')
50.  ba'@0  \mcong{}  b'x1
51.  bc'@0  \mcong{}  b'z'
52.  a'@0  leftof  bp
53.  c'@0  leftof  pb
54.  x1  leftof  b'p'
55.  z'  leftof  p'b'
56.  a'@0ba1  \mcong{}\msuba{}  x1b'x'
57.  a1bc'@0  \mcong{}\msuba{}  x'b'z'
\mvdash{}  a'@0c'@0  \mcong{}  x1z'


By

---

Latex:
(Assert  x'  \#  z'  BY
              ((InstLemma  `lsep-iff-all-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ((D  -1  THEN  D  -2)  THENA  (Unfold  `geo-lsep`  0  THEN  Auto))
                THEN  D  -1
                THEN  InstHyp  [\mkleeneopen{}x'\mkleeneclose{}]  (-2)\mcdot{}
                THEN  Auto))

---

Home Index