---

Step * 1 1 of Lemma Euclid-prop16


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. b-c-d
8. ∃x:{x:Point| b=x=c} . ∃y:{y:Point| a=x=y} . (abc ≅a ycb ∧ (b # x ∧ x # c) ∧ a # x ∧ x # y)
⊢ cba < acd
BY
{ (((gProperProlong ⌜a⌝⌜c⌝`g\''⌜O⌝⌜X⌝⋅ THENA Auto) THEN ExRepD)
   THEN (Assert x # ac BY
               ((InstLemma `colinear-lsep` [⌜g⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜x⌝]⋅ THEN Auto) THEN D 8 THEN Auto))
   THEN (Assert g'-c-a ∧ y-x-a BY
               ((((D 8 THEN D 10) THEN Unhide) THEN Auto) THEN D 0 THEN EAuto 1))) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. b-c-d
8. x : {x:Point| b=x=c} 
9. y : {y:Point| a=x=y} 
10. abc ≅a ycb
11. b # x
12. x # c
13. a # x
14. x # y
15. g' : Point
16. a-c-g'
17. cg' ≅ OX
18. x # ac
19. g'-c-a ∧ y-x-a
⊢ cba < acd

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  a  \#  bc
7.  b-c-d
8.  \mexists{}x:\{x:Point|  b=x=c\}  .  \mexists{}y:\{y:Point|  a=x=y\}  .  (abc  \mcong{}\msuba{}  ycb  \mwedge{}  (b  \#  x  \mwedge{}  x  \#  c)  \mwedge{}  a  \#  x  \mwedge{}  x  \#  y)
\mvdash{}  cba  <  acd


By

---

Latex:
(((gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`g\mbackslash{}''\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (Assert  x  \#  ac  BY
                          ((InstLemma  `colinear-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  8  THEN  Auto))
  THEN  (Assert  g'-c-a  \mwedge{}  y-x-a  BY
                          ((((D  8  THEN  D  10)  THEN  Unhide)  THEN  Auto)  THEN  D  0  THEN  EAuto  1)))

---

Home Index