---

Step * 1 of Lemma vertical-angles-congruent


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. a-b-a'
8. c-b-c'
⊢ ∃a'@0,c'@0,x',z':Point. (b_a_a'@0 ∧ b_c_c'@0 ∧ b_a'_x' ∧ b_c'_z' ∧ ba'@0 ≅ bx' ∧ bc'@0 ≅ bz' ∧ a'@0c'@0 ≅ x'z')
BY
{ ((((gProperProlong ⌜b⌝⌜a'⌝`A\''⌜a⌝⌜b⌝⋅ THENA Auto) THEN (gProperProlong ⌜b⌝⌜a⌝`A'⌜b⌝⌜a'⌝⋅ THENA Auto))
    THEN (gProperProlong ⌜b⌝⌜c'⌝`C\''⌜b⌝⌜c⌝⋅ THENA Auto)
    THEN (gProperProlong ⌜b⌝⌜c⌝`C'⌜b⌝⌜c'⌝⋅ THENA Auto))
   THEN (InstLemma `geo-midpoint-diagonals-congruent` [⌜e⌝;⌜b⌝;⌜A⌝;⌜C⌝;⌜A'⌝;⌜C'⌝]⋅
         THENA (Auto THEN Unfold `geo-midpoint` 0 THEN Auto)
         )
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. a-b-a'
8. c-b-c'
9. A' : Point
10. b-a'-A' ∧ a'A' ≅ ab
11. A : Point
12. b-a-A ∧ aA ≅ ba'
13. C' : Point
14. b-c'-C' ∧ c'C' ≅ bc
15. C : Point
16. b-c-C ∧ cC ≅ bc'
17. AC ≅ A'C'
⊢ ∃a'@0,c'@0,x',z':Point. (b_a_a'@0 ∧ b_c_c'@0 ∧ b_a'_x' ∧ b_c'_z' ∧ ba'@0 ≅ bx' ∧ bc'@0 ≅ bz' ∧ a'@0c'@0 ≅ x'z')

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  c'  :  Point
7.  a-b-a'
8.  c-b-c'
\mvdash{}  \mexists{}a'@0,c'@0,x',z':Point
      (b\_a\_a'@0  \mwedge{}  b\_c\_c'@0  \mwedge{}  b\_a'\_x'  \mwedge{}  b\_c'\_z'  \mwedge{}  ba'@0  \mcong{}  bx'  \mwedge{}  bc'@0  \mcong{}  bz'  \mwedge{}  a'@0c'@0  \mcong{}  x'z')


By

---

Latex:
((((gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}`A\mbackslash{}''\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)
      THEN  (gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`A'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}\mcdot{}  THENA  Auto)
      )
    THEN  (gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c'\mkleeneclose{}`C\mbackslash{}''\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  (gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`C'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c'\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  (InstLemma  `geo-midpoint-diagonals-congruent`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}A'\mkleeneclose{};\mkleeneopen{}C'\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Unfold  `geo-midpoint`  0  THEN  Auto)
              )
  )

---

Home Index