---

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


1. e : EuclideanPlane
2. x : {p:Point| O_X_p} 
3. y : {p:Point| O_X_p} 
4. z : {p:Point| O_X_p} 
⊢ x + y + z = x + y + z ∈ Point
BY
{ (DSetVars
   THEN Unfold `eu-add-length` 0
   THEN (Assert ¬(O = X ∈ Point) BY
               Auto)
   THEN (Assert ¬(O = x ∈ Point) BY
               (NotEqualFromEuBetween⋅ THEN Auto))
   THEN (Assert ¬(O = y ∈ Point) BY
               (NotEqualFromEuBetween⋅ THEN Auto))
   THEN GeneralizeEuExtends [`a'; `b'; `c']⋅
   THEN (Assert ¬(O = c ∈ Point) BY
               (NotEqualFromEuBetween⋅ THEN Auto))
   THEN GeneralizeEuExtends [`d']) }

1
1. e : EuclideanPlane
2. x : Point
3. O_X_x
4. y : Point
5. O_X_y
6. z : Point
7. O_X_z
8. ¬(O = X ∈ Point)
9. ¬(O = x ∈ Point)
10. ¬(O = y ∈ Point)
11. a : Point@i
12. O_y_a ∧ ya=Xz@i
13. b : Point@i
14. O_x_b ∧ xb=Xa@i
15. c : Point@i
16. O_x_c ∧ xc=Xy@i
17. ¬(O = c ∈ Point)
18. d : Point@i
19. O_c_d ∧ cd=Xz@i
⊢ b = d ∈ Point

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  x  :  \{p:Point|  O\_X\_p\} 
3.  y  :  \{p:Point|  O\_X\_p\} 
4.  z  :  \{p:Point|  O\_X\_p\} 
\mvdash{}  x  +  y  +  z  =  x  +  y  +  z


By

---

Latex:
(DSetVars
  THEN  Unfold  `eu-add-length`  0
  THEN  (Assert  \mneg{}(O  =  X)  BY
                          Auto)
  THEN  (Assert  \mneg{}(O  =  x)  BY
                          (NotEqualFromEuBetween\mcdot{}  THEN  Auto))
  THEN  (Assert  \mneg{}(O  =  y)  BY
                          (NotEqualFromEuBetween\mcdot{}  THEN  Auto))
  THEN  GeneralizeEuExtends  [`a';  `b';  `c']\mcdot{}
  THEN  (Assert  \mneg{}(O  =  c)  BY
                          (NotEqualFromEuBetween\mcdot{}  THEN  Auto))
  THEN  GeneralizeEuExtends  [`d'])

---

Home Index