---

Step * 1 of Lemma Euclid-Prop20


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. d : Point
7. b-a-d
8. adc ≅a acd
9. ad ≅ ac
⊢ |bc| < |ba| + |ac|
BY
{ (Assert adc < bcd BY
         ((InstLemma `Euclid-Prop18-lemma` [⌜e⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto)
          THEN ((FLemma `geo-cong-angle-symm2` [-3] THENA Auto) THEN (FLemma `geo-lt-angle-symm2` [-2] THENA Auto))
          THEN (InstLemma `geo-cong-angle-preserves-lt-angle` [⌜e⌝;⌜a⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜d⌝;⌜c⌝;⌜d⌝;⌜c⌝;⌜b⌝]⋅ THEN Auto)
          THEN FLemma `geo-lt-angle-symm` [-1]
          THEN Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. d : Point
7. b-a-d
8. adc ≅a acd
9. ad ≅ ac
10. adc < bcd
⊢ |bc| < |ba| + |ac|

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  d  :  Point
7.  b-a-d
8.  adc  \mcong{}\msuba{}  acd
9.  ad  \mcong{}  ac
\mvdash{}  |bc|  <  |ba|  +  |ac|


By

---

Latex:
(Assert  adc  <  bcd  BY
              ((InstLemma  `Euclid-Prop18-lemma`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)
                THEN  ((FLemma  `geo-cong-angle-symm2`  [-3]  THENA  Auto)
                            THEN  (FLemma  `geo-lt-angle-symm2`  [-2]  THENA  Auto)
                            )
                THEN  (InstLemma  `geo-cong-angle-preserves-lt-angle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}
                            ]\mcdot{}
                            THEN  Auto
                            )
                THEN  FLemma  `geo-lt-angle-symm`  [-1]
                THEN  Auto))

---

Home Index