---

Step * of Lemma geo-gt-implies-point

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (ab > cd ⇒ c ≠ d ⇒ (¬¬(∃f:Point. (c-d-f ∧ cf ≅ ab))))
BY
{ (((Auto THEN Unfold `geo-gt` -2) THEN Auto)
   THEN ExRepD
   THEN ((gProperProlong ⌜d⌝⌜c⌝`P'⌜O⌝⌜X⌝⋅ THENA Auto) THEN ExRepD)
   THEN (gProperProlong ⌜P⌝⌜c⌝`d1'⌜a⌝⌜w⌝⋅ THENA Auto)
   THEN (Assert d1 ≡ d BY
               (InstLemma `geo-construction-unicity` [⌜e⌝;⌜P⌝;⌜c⌝;⌜d⌝;⌜d1⌝]⋅ THEN Auto))
   THEN (gProperProlong ⌜c⌝⌜d⌝`f'⌜w⌝⌜b⌝⋅ THENA Auto)
   THEN RemoveDoubleNegation
   THEN D 0 With ⌜f⌝ 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (ab  >  cd  {}\mRightarrow{}  c  \mneq{}  d  {}\mRightarrow{}  (\mneg{}\mneg{}(\mexists{}f:Point.  (c-d-f  \mwedge{}  cf  \mcong{}  ab))))


By

---

Latex:
(((Auto  THEN  Unfold  `geo-gt`  -2)  THEN  Auto)
  THEN  ExRepD
  THEN  ((gProperProlong  \mkleeneopen{}d\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`P'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (gProperProlong  \mkleeneopen{}P\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`d1'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}w\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  d1  \mequiv{}  d  BY
                          (InstLemma  `geo-construction-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (gProperProlong  \mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}`f'\mkleeneopen{}w\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RemoveDoubleNegation
  THEN  D  0  With  \mkleeneopen{}f\mkleeneclose{} 
  THEN  Auto)

---

Home Index