---

Step * 1 1 of Lemma cong-angle-between-exists-iff


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. b_a_a'
17. b_c_c'
18. y_x_x'
19. y_z_z'
20. ba' ≅ yx'
21. bc' ≅ yz'
22. a'c' ≅ x'z'
23. X : Point
24. y-x-X
25. xX ≅ ba
26. A : Point
27. b-a-A
28. aA ≅ yx
29. Z : Point
30. y-z-Z
31. zZ ≅ bc
32. C : Point
33. b-c-C
34. cC ≅ yz
⊢ ∃a',c',x',z':Point
   ((((b_a_a' ∧ b_c_c') ∧ y_x_x') ∧ y_z_z') ∧ (((ba ≅ xx' ∧ aa' ≅ yx) ∧ bc ≅ zz') ∧ cc' ≅ yz) ∧ a'c' ≅ x'z')
BY
{ ((InstConcl [⌜A⌝;⌜C⌝;⌜X⌝;⌜Z⌝]⋅ THEN Auto)
   THEN (InstLemma `geo-colinear-five-segment` [⌜e⌝;⌜b⌝;⌜a'⌝;⌜A⌝;⌜c'⌝;⌜y⌝;⌜x'⌝;⌜X⌝;⌜z'⌝]⋅
         THENA (Auto THEN InstLemma `out-congruent` [⌜e⌝;⌜b⌝;⌜y⌝;⌜a⌝;⌜a'⌝;⌜A⌝;⌜x⌝;⌜x'⌝;⌜X⌝]⋅ THEN EAuto 1)
         )
   THEN (InstLemma `geo-colinear-five-segment` [⌜e⌝;⌜b⌝;⌜c'⌝;⌜C⌝;⌜A⌝;⌜y⌝;⌜z'⌝;⌜Z⌝;⌜X⌝]⋅ THEN Auto)
   THEN InstLemma `out-congruent` [⌜e⌝;⌜b⌝;⌜y⌝;⌜c⌝;⌜c'⌝;⌜C⌝;⌜z⌝;⌜z'⌝;⌜Z⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  b  \mneq{}  a
9.  b  \mneq{}  c
10.  y  \mneq{}  x
11.  y  \mneq{}  z
12.  a'  :  Point
13.  c'  :  Point
14.  x'  :  Point
15.  z'  :  Point
16.  b\_a\_a'
17.  b\_c\_c'
18.  y\_x\_x'
19.  y\_z\_z'
20.  ba'  \mcong{}  yx'
21.  bc'  \mcong{}  yz'
22.  a'c'  \mcong{}  x'z'
23.  X  :  Point
24.  y-x-X
25.  xX  \mcong{}  ba
26.  A  :  Point
27.  b-a-A
28.  aA  \mcong{}  yx
29.  Z  :  Point
30.  y-z-Z
31.  zZ  \mcong{}  bc
32.  C  :  Point
33.  b-c-C
34.  cC  \mcong{}  yz
\mvdash{}  \mexists{}a',c',x',z':Point
      ((((b\_a\_a'  \mwedge{}  b\_c\_c')  \mwedge{}  y\_x\_x')  \mwedge{}  y\_z\_z')
      \mwedge{}  (((ba  \mcong{}  xx'  \mwedge{}  aa'  \mcong{}  yx)  \mwedge{}  bc  \mcong{}  zz')  \mwedge{}  cc'  \mcong{}  yz)
      \mwedge{}  a'c'  \mcong{}  x'z')


By

---

Latex:
((InstConcl  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `geo-colinear-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  InstLemma  `out-congruent`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}
                            THEN  EAuto  1)
              )
  THEN  (InstLemma  `geo-colinear-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstLemma  `out-congruent`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index