---

Step * 1 of Lemma supplementary-angles-preserve-congruence


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. d' : Point
10. a ≠ b
11. b ≠ c
12. d ≠ e
13. e ≠ f
14. a1 : Point
15. c' : Point
16. x' : Point
17. z' : Point
18. b_a_a1
19. b_c_c'
20. e_d_x'
21. e_f_z'
22. ba1 ≅ ex'
23. bc' ≅ ez'
24. a1c' ≅ x'z'
25. a-b-a'
26. d-e-d'
⊢ ∃a'@0,c',x',z':Point. (b_a'_a'@0 ∧ b_c_c' ∧ e_d'_x' ∧ e_f_z' ∧ ba'@0 ≅ ex' ∧ bc' ≅ ez' ∧ a'@0c' ≅ x'z')
BY
{ ((gProperProlong ⌜e⌝⌜d'⌝`d\'\''⌜b⌝⌜a'⌝⋅ THENA Auto)
   THEN (gProperProlong ⌜b⌝⌜a'⌝`a\'\''⌜e⌝⌜d'⌝⋅ THENA Auto)
   THEN (InstConcl [⌜a''⌝;⌜c'⌝;⌜d''⌝;⌜z'⌝]⋅ THEN Auto)
   THEN InstLemma `geo-five-segment` [⌜g⌝;⌜a1⌝;⌜b⌝;⌜a''⌝;⌜c'⌝;⌜x'⌝;⌜e⌝;⌜d''⌝;⌜z'⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  a'  :  Point
9.  d'  :  Point
10.  a  \mneq{}  b
11.  b  \mneq{}  c
12.  d  \mneq{}  e
13.  e  \mneq{}  f
14.  a1  :  Point
15.  c'  :  Point
16.  x'  :  Point
17.  z'  :  Point
18.  b\_a\_a1
19.  b\_c\_c'
20.  e\_d\_x'
21.  e\_f\_z'
22.  ba1  \mcong{}  ex'
23.  bc'  \mcong{}  ez'
24.  a1c'  \mcong{}  x'z'
25.  a-b-a'
26.  d-e-d'
\mvdash{}  \mexists{}a'@0,c',x',z':Point
      (b\_a'\_a'@0  \mwedge{}  b\_c\_c'  \mwedge{}  e\_d'\_x'  \mwedge{}  e\_f\_z'  \mwedge{}  ba'@0  \mcong{}  ex'  \mwedge{}  bc'  \mcong{}  ez'  \mwedge{}  a'@0c'  \mcong{}  x'z')


By

---

Latex:
((gProperProlong  \mkleeneopen{}e\mkleeneclose{}\mkleeneopen{}d'\mkleeneclose{}`d\mbackslash{}'\mbackslash{}''\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}`a\mbackslash{}'\mbackslash{}''\mkleeneopen{}e\mkleeneclose{}\mkleeneopen{}d'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstConcl  [\mkleeneopen{}a''\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}d''\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstLemma  `geo-five-segment`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a''\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d''\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index