---

Step * 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 ∧ B(OXx)
9. y : {x:Point| B(OXx) ∧ Xx ≅ ab} 
10. Xy ≅ ab ∧ B(OXy)
11. z : {x:Point| B(OXx) ∧ Xx ≅ bc} 
12. Xz ≅ bc ∧ B(OXz)
⊢ x ≡ extend Oy by Xz
BY
{ (gSeparatedCases' ⌜O⌝ ⌜y⌝⋅ 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 ∧ B(OXx)
9. y : {x:Point| B(OXx) ∧ Xx ≅ ab} 
10. Xy ≅ ab ∧ B(OXy)
11. z : {x:Point| B(OXx) ∧ Xx ≅ bc} 
12. Xz ≅ bc ∧ B(OXz)
13. O # y
⊢ x ≡ extend Oy by Xz

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. y : {x:Point| B(OXx) ∧ Xx ≅ ab} 
5. c : Point
6. B(abc)
7. y # X
8. x : {x:Point| B(OXx) ∧ Xx ≅ ac} 
9. Xx ≅ ac
10. B(yXx)
11. Xy ≅ ab
12. B(yXy)
13. z : {x:Point| B(OXx) ∧ Xx ≅ bc} 
14. Xz ≅ bc
15. B(yXz)
16. O ≡ y
⊢ x ≡ extend Oy by Xz

---

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  \mwedge{}  B(OXx)
9.  y  :  \{x:Point|  B(OXx)  \mwedge{}  Xx  \mcong{}  ab\} 
10.  Xy  \mcong{}  ab  \mwedge{}  B(OXy)
11.  z  :  \{x:Point|  B(OXx)  \mwedge{}  Xx  \mcong{}  bc\} 
12.  Xz  \mcong{}  bc  \mwedge{}  B(OXz)
\mvdash{}  x  \mequiv{}  extend  Oy  by  Xz


By

---

Latex:
(gSeparatedCases'  \mkleeneopen{}O\mkleeneclose{}  \mkleeneopen{}y\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index