---

Step * of Lemma geo-add-length-between

∀[e:BasicGeometry]. ∀[a,b,c:Point].  |ac| = |ab| + |bc| ∈ Length supposing B(abc)
BY
{ ((Auto THEN EqTypeCD THEN Auto)
   THEN Unfold `geo-add-length` 0
   THEN (Assert O # X BY
               Auto)
   THEN Unfold `geo-length` 0
   THEN Reduce 0
   THEN GeneralizeGeoExtends [`x';`y';`z']) }

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)
⊢ x ≡ extend Oy by Xz

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[a,b,c:Point].    |ac|  =  |ab|  +  |bc|  supposing  B(abc)


By

---

Latex:
((Auto  THEN  EqTypeCD  THEN  Auto)
  THEN  Unfold  `geo-add-length`  0
  THEN  (Assert  O  \#  X  BY
                          Auto)
  THEN  Unfold  `geo-length`  0
  THEN  Reduce  0
  THEN  GeneralizeGeoExtends  [`x';`y';`z'])

---

Home Index