---

Step * of Lemma zero-angles-congruent

∀g:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (b ≠ a ⇒ y ≠ x ⇒ b_a_c ⇒ y_x_z ⇒ abc ≅a xyz)
BY
{ (((Auto THEN Unfold `geo-cong-angle` 0) THEN GenRepD THEN Auto)
   THEN ((gProperProlong  ⌜b⌝⌜a⌝`A'⌜y⌝⌜x⌝⋅ THENA Auto)
         THEN (Assert b ≠ c BY
                     (FLemma `geo-between-sep` [10] THEN Auto))
         THEN (Assert y ≠ z BY
                     (FLemma `geo-between-sep` [11] THEN Auto)))
   THEN (gProperProlong  ⌜b⌝⌜c⌝`C'⌜y⌝⌜z⌝⋅ THENA Auto)
   THEN (gProperProlong  ⌜y⌝⌜x⌝`X'⌜a⌝⌜b⌝⋅ THENA Auto)
   THEN (gProperProlong  ⌜y⌝⌜z⌝`Z'⌜b⌝⌜c⌝⋅ THENA Auto)
   THEN InstConcl [⌜A⌝;⌜C⌝;⌜X⌝;⌜Z⌝]⋅
   THEN Auto) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. y ≠ x
10. b_a_c
11. y_x_z
12. A : Point
13. b-a-A
14. aA ≅ yx
15. b ≠ c
16. y ≠ z
17. C : Point
18. b-c-C
19. cC ≅ yz
20. X : Point
21. y-x-X
22. xX ≅ ab
23. Z : Point
24. y-z-Z
25. zZ ≅ bc
26. b_a_A
27. b_c_C
28. y_x_X
29. y_z_Z
30. bA ≅ yX
31. bC ≅ yZ
⊢ AC ≅ XZ

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.    (b  \mneq{}  a  {}\mRightarrow{}  y  \mneq{}  x  {}\mRightarrow{}  b\_a\_c  {}\mRightarrow{}  y\_x\_z  {}\mRightarrow{}  abc  \mcong{}\msuba{}  xyz)


By

---

Latex:
(((Auto  THEN  Unfold  `geo-cong-angle`  0)  THEN  GenRepD  THEN  Auto)
  THEN  ((gProperProlong    \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`A'\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (Assert  b  \mneq{}  c  BY
                                      (FLemma  `geo-between-sep`  [10]  THEN  Auto))
              THEN  (Assert  y  \mneq{}  z  BY
                                      (FLemma  `geo-between-sep`  [11]  THEN  Auto)))
  THEN  (gProperProlong    \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`C'\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong    \mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}`X'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong    \mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}z\mkleeneclose{}`Z'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index