---

Step * 1 1 of Lemma eu-add-length-between


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a_b_c
6. ¬(O = X ∈ Point)
⊢ |ac| = (extend O|ab| by X|bc|) ∈ Point
BY
{ (Unfold `eu-length` 0
   THEN Reduce 0
   THEN GeneralizeEuExtends [`x'; `y'; `z']⋅
   THEN (Assert ¬(O = y ∈ Point) BY
               (NotEqualFromEuBetween⋅ THEN Auto))
   THEN GeneralizeEuExtends [`w']⋅
   THEN InstLemma `eu-construction-unicity` [⌜e⌝;⌜O⌝;⌜X⌝;⌜x⌝;⌜w⌝]⋅
   THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a_b_c
6. ¬(O = X ∈ Point)
7. x : Point
8. O_X_x
9. Xx=ac
10. y : Point
11. O_X_y
12. Xy=ab
13. z : Point
14. O_X_z
15. Xz=bc
16. ¬(O = y ∈ Point)
17. w : Point
18. O_y_w
19. yw=Xz
⊢ Xw=Xx

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a\_b\_c
6.  \mneg{}(O  =  X)
\mvdash{}  |ac|  =  (extend  O|ab|  by  X|bc|)


By

---

Latex:
(Unfold  `eu-length`  0
  THEN  Reduce  0
  THEN  GeneralizeEuExtends  [`x';  `y';  `z']\mcdot{}
  THEN  (Assert  \mneg{}(O  =  y)  BY
                          (NotEqualFromEuBetween\mcdot{}  THEN  Auto))
  THEN  GeneralizeEuExtends  [`w']\mcdot{}
  THEN  InstLemma  `eu-construction-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index