---

Step * of Lemma geo-gt-prim-implies-lt

No Annotations
∀e:EuclideanPlane. ∀a,b,c,d:Point.  (ab>cd ⇒ |cd| < |ab|)
BY
{ (Auto
   THEN (Unfold `geo-lt` 0 THEN Auto)
   THEN (Assert a # b BY
               ((Unfold `geo-sep` 0 THENA Auto)
                THEN UseGeoAxioms
                THEN InstHyp [⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜a⌝] (10)⋅
                THEN Auto))) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab>cd
7. a # b
⊢ ∃a@0,b@0:Point. (a@0 # b@0 ∧ |cd| + |a@0b@0| ≤ |ab|)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (ab>cd  {}\mRightarrow{}  |cd|  <  |ab|)


By

---

Latex:
(Auto
  THEN  (Unfold  `geo-lt`  0  THEN  Auto)
  THEN  (Assert  a  \#  b  BY
                          ((Unfold  `geo-sep`  0  THENA  Auto)
                            THEN  UseGeoAxioms
                            THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  (10)\mcdot{}
                            THEN  Auto)))

---

Home Index