---

Step * 1 of Lemma Euclid-Prop16-construction-lemma


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. d : Point
7. b=d=c
8. d # ca
9. y : Point
10. a-d-y
11. dy ≅ ad
⊢ abc ≅a ycb
BY
{ (((Assert b-d-c BY
           (D 0 THEN Auto))
    THEN (Assert y ≠ c BY
                (InstLemma `colinear-lsep` [⌜g⌝;⌜d⌝;⌜a⌝;⌜c⌝;⌜y⌝]⋅ THEN EAuto 1))
    )
   THEN (Assert abd ≅a ycd BY
               ((Unfold `geo-cong-angle` 0 THEN Auto)
                THEN (InstConcl [⌜a⌝;⌜d⌝;⌜y⌝;⌜d⌝]⋅ THEN Auto)
                THEN (D 7 THEN Auto)
                THEN (InstLemma `vertical-angles-congruent` [⌜g⌝;⌜a⌝;⌜d⌝;⌜b⌝;⌜y⌝;⌜c⌝]⋅ THENA Auto)
                THEN InstLemma `geo-sas2` [⌜g⌝;⌜d⌝;⌜a⌝;⌜b⌝;⌜d⌝;⌜y⌝;⌜c⌝]⋅
                THEN Auto))
   ) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. d : Point
7. b=d=c
8. d # ca
9. y : Point
10. a-d-y
11. dy ≅ ad
12. b-d-c
13. y ≠ c
14. abd ≅a ycd
⊢ abc ≅a ycb

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  d  :  Point
7.  b=d=c
8.  d  \#  ca
9.  y  :  Point
10.  a-d-y
11.  dy  \mcong{}  ad
\mvdash{}  abc  \mcong{}\msuba{}  ycb


By

---

Latex:
(((Assert  b-d-c  BY
                  (D  0  THEN  Auto))
    THEN  (Assert  y  \mneq{}  c  BY
                            (InstLemma  `colinear-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  EAuto  1))
    )
  THEN  (Assert  abd  \mcong{}\msuba{}  ycd  BY
                          ((Unfold  `geo-cong-angle`  0  THEN  Auto)
                            THEN  (InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THEN  (D  7  THEN  Auto)
                            THEN  (InstLemma  `vertical-angles-congruent`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  InstLemma  `geo-sas2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  )

---

Home Index