---

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


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. B(abc)
6. O # X
7. x : {x:Point| B(OXx) ∧ Xx ≅ ac} 
8. Xx ≅ ac
9. B(OXx)
10. y : {x:Point| B(OXx) ∧ Xx ≅ ab} 
11. Xy ≅ ab
12. B(OXy)
13. z : {x:Point| B(OXx) ∧ Xx ≅ bc} 
14. Xz ≅ bc
15. B(OXz)
16. O # y
17. w : {x:Point| B(Oyx) ∧ yx ≅ Xz} 
18. yw ≅ Xz
19. B(Oyw)
⊢ Xw ≅ Xx
BY
{ (gSeparatedCases ⌜a⌝ ⌜b⌝⋅ THENA Auto) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. B(abc)
6. O # X
7. x : {x:Point| B(OXx) ∧ Xx ≅ ac} 
8. Xx ≅ ac
9. B(OXx)
10. y : {x:Point| B(OXx) ∧ Xx ≅ ab} 
11. Xy ≅ ab
12. B(OXy)
13. z : {x:Point| B(OXx) ∧ Xx ≅ bc} 
14. Xz ≅ bc
15. B(OXz)
16. O # y
17. w : {x:Point| B(Oyx) ∧ yx ≅ Xz} 
18. yw ≅ Xz
19. B(Oyw)
20. a # b
⊢ Xw ≅ Xx

2
1. e : BasicGeometry
2. b : Point
3. a : Point
4. c : Point
5. B(bbc)
6. O # X
7. x : {x:Point| B(OXx) ∧ Xx ≅ ac} 
8. Xx ≅ bc
9. B(OXx)
10. y : {x:Point| B(OXx) ∧ Xx ≅ ab} 
11. Xy ≅ bb
12. B(OXy)
13. z : {x:Point| B(OXx) ∧ Xx ≅ bc} 
14. Xz ≅ bc
15. B(OXz)
16. O # y
17. w : {x:Point| B(Oyx) ∧ yx ≅ Xz} 
18. yw ≅ Xz
19. B(Oyw)
20. a ≡ b
⊢ Xw ≅ Xx

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  B(abc)
6.  O  \#  X
7.  x  :  \{x:Point|  B(OXx)  \mwedge{}  Xx  \mcong{}  ac\} 
8.  Xx  \mcong{}  ac
9.  B(OXx)
10.  y  :  \{x:Point|  B(OXx)  \mwedge{}  Xx  \mcong{}  ab\} 
11.  Xy  \mcong{}  ab
12.  B(OXy)
13.  z  :  \{x:Point|  B(OXx)  \mwedge{}  Xx  \mcong{}  bc\} 
14.  Xz  \mcong{}  bc
15.  B(OXz)
16.  O  \#  y
17.  w  :  \{x:Point|  B(Oyx)  \mwedge{}  yx  \mcong{}  Xz\} 
18.  yw  \mcong{}  Xz
19.  B(Oyw)
\mvdash{}  Xw  \mcong{}  Xx


By

---

Latex:
(gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index