---

Step * of Lemma Euclid-Prop20

∀e:EuclideanPlane. ∀a,b,c:Point.  (a # bc ⇒ |bc| < |ba| + |ac|)
BY
{ (Auto
   THEN (Assert ∃d:Point. (b-a-d ∧ adc ≅a acd ∧ ad ≅ ac) BY
               (((gProperProlong ⌜b⌝⌜a⌝`d'⌜a⌝⌜c⌝⋅ THEN Auto)
                 THEN (Assert d ≠ c BY
                             (InstLemma  `colinear-lsep` [⌜e⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜d⌝]⋅ THEN Auto))
                 )
                THEN (InstLemma `Euclid-Prop5_1` [⌜e⌝;⌜a⌝;⌜d⌝;⌜c⌝]⋅ THEN Auto)
                THEN D 0
                THEN Auto))
   THEN ExRepD) }

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
⊢ |bc| < |ba| + |ac|

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  |bc|  <  |ba|  +  |ac|)


By

---

Latex:
(Auto
  THEN  (Assert  \mexists{}d:Point.  (b-a-d  \mwedge{}  adc  \mcong{}\msuba{}  acd  \mwedge{}  ad  \mcong{}  ac)  BY
                          (((gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`d'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THEN  Auto)
                              THEN  (Assert  d  \mneq{}  c  BY
                                                      (InstLemma    `colinear-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto))
                              )
                            THEN  (InstLemma  `Euclid-Prop5\_1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THEN  D  0
                            THEN  Auto))
  THEN  ExRepD)

---

Home Index