---

Step * of Lemma Euclid-Prop25

∀p:EuclideanPlane. ∀a,b,c,d,e,f:Point.  (a # bc ⇒ d # ef ⇒ ab ≅ de ⇒ ac ≅ df ⇒ |ef| < |bc| ⇒ edf < bac)
BY
{ (Auto
   THEN (Assert ∃g:Point. (e-f-g ∧ eg ≅ bc) BY
               (InstLemma  `geo-lt-implies-point` [⌜p⌝;⌜e⌝;⌜f⌝;⌜b⌝;⌜c⌝]⋅ THEN Auto))
   THEN (Assert f leftof ed ∨ f leftof de BY
               (FLemma  `lsep-all-sym` [9] THEN Auto))
   THEN D -1) }

1
1. p : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a # bc
9. d # ef
10. ab ≅ de
11. ac ≅ df
12. |ef| < |bc|
13. ∃g:Point. (e-f-g ∧ eg ≅ bc)
14. f leftof ed
⊢ edf < bac

2
1. p : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a # bc
9. d # ef
10. ab ≅ de
11. ac ≅ df
12. |ef| < |bc|
13. ∃g:Point. (e-f-g ∧ eg ≅ bc)
14. f leftof de
⊢ edf < bac

---

Latex:

---

Latex:
\mforall{}p:EuclideanPlane.  \mforall{}a,b,c,d,e,f:Point.
    (a  \#  bc  {}\mRightarrow{}  d  \#  ef  {}\mRightarrow{}  ab  \mcong{}  de  {}\mRightarrow{}  ac  \mcong{}  df  {}\mRightarrow{}  |ef|  <  |bc|  {}\mRightarrow{}  edf  <  bac)


By

---

Latex:
(Auto
  THEN  (Assert  \mexists{}g:Point.  (e-f-g  \mwedge{}  eg  \mcong{}  bc)  BY
                          (InstLemma    `geo-lt-implies-point`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (Assert  f  leftof  ed  \mvee{}  f  leftof  de  BY
                          (FLemma    `lsep-all-sym`  [9]  THEN  Auto))
  THEN  D  -1)

---

Home Index