---

Step * 1 of Lemma Euclid-Prop19


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. bca < abc
7. d : Point
8. b=d=c
9. d # ba
10. ∃E:Point. (a=d=E ∧ bE ≅ ca)
⊢ |ab| < |ac|
BY
{ (ExRepD
   THEN (Assert dbE < abd BY
               ((Assert dbE ≅a dca BY
                       (Unfold `geo-cong-angle` 0
                        THEN (Assert b ≠ E BY
                                    (InstLemma `colinear-lsep` [⌜e⌝;⌜d⌝;⌜a⌝;⌜b⌝;⌜E⌝]⋅ THEN Auto))
                        THEN (GenRepD THEN Auto)
                        THEN (InstConcl [⌜d⌝;⌜E⌝;⌜d⌝;⌜a⌝]⋅ THEN EAuto 1)
                        THEN D -9
                        THEN Auto))
                THEN (Assert dbE ≅a bca BY
                            ((InstLemma `out-preserves-angle-cong_1` [⌜e⌝;⌜d⌝;⌜b⌝;⌜E⌝;⌜d⌝;⌜c⌝;⌜a⌝;⌜d⌝;⌜E⌝;⌜b⌝;⌜a⌝]⋅
                              THEN EAuto 1
                              )
                             THEN D -6
                             THEN InstLemma `geo-between-out` [⌜e⌝]⋅
                             THEN EAuto 1))
                THEN (Assert abc ≅a abd BY
                            ((InstLemma `out-cong-angle` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜d⌝]⋅ THENA Auto)
                             THEN D -7
                             THEN InstLemma `geo-between-out` [⌜e⌝;⌜b⌝;⌜d⌝;⌜c⌝]⋅
                             THEN EAuto 1))
                THEN (InstLemma `geo-cong-angle-preserves-lt-angle2` [⌜e⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜a⌝;⌜b⌝;⌜d⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅
                      THEN EAuto 1
                      )
                THEN InstLemma `geo-cong-angle-preserves-lt-angle` [⌜e⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜d⌝;⌜b⌝;⌜E⌝;⌜a⌝;⌜b⌝;⌜d⌝]⋅
                THEN EAuto 1))
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. bca < abc
7. d : Point
8. b=d=c
9. d # ba
10. E : Point
11. a=d=E
12. bE ≅ ca
13. dbE < abd
⊢ |ab| < |ac|

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  bca  <  abc
7.  d  :  Point
8.  b=d=c
9.  d  \#  ba
10.  \mexists{}E:Point.  (a=d=E  \mwedge{}  bE  \mcong{}  ca)
\mvdash{}  |ab|  <  |ac|


By

---

Latex:
(ExRepD
  THEN  (Assert  dbE  <  abd  BY
                          ((Assert  dbE  \mcong{}\msuba{}  dca  BY
                                          (Unfold  `geo-cong-angle`  0
                                            THEN  (Assert  b  \mneq{}  E  BY
                                                                    (InstLemma  `colinear-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{}]\mcdot{}  THEN  Auto))
                                            THEN  (GenRepD  THEN  Auto)
                                            THEN  (InstConcl  [\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
                                            THEN  D  -9
                                            THEN  Auto))
                            THEN  (Assert  dbE  \mcong{}\msuba{}  bca  BY
                                                    ((InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};
                                                        \mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
                                                        THEN  EAuto  1
                                                        )
                                                      THEN  D  -6
                                                      THEN  InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
                                                      THEN  EAuto  1))
                            THEN  (Assert  abc  \mcong{}\msuba{}  abd  BY
                                                    ((InstLemma  `out-cong-angle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                                      THEN  D  -7
                                                      THEN  InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
                                                      THEN  EAuto  1))
                            THEN  (InstLemma  `geo-cong-angle-preserves-lt-angle2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};
                                        \mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
                                        THEN  EAuto  1
                                        )
                            THEN  InstLemma  `geo-cong-angle-preserves-lt-angle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};
                            \mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}
                            THEN  EAuto  1))
  )

---

Home Index