---

Step * 1 1 3 1 1 1 1 of Lemma colinear-implies-midpoint


1. e : BasicGeometry
2. M : Point
3. A : Point
4. B : Point
5. A # B
6. Colinear(A;M;B)
7. MA ≅ MB
8. B-A-M
9. B(BAM)
10. |BM| = |BA| + |BM| ∈ Length
11. |AM| = |BM| ∈ Length
12. |BM| + X = |BA| + |BM| ∈ Length
⊢ B(AMB)
BY
{ (Fold `geo-zero-length` (-1) THEN (RW (AddrC [2] (LemmaC `geo-add-length-comm`)) (-1) THENA Auto)) }

1
1. e : BasicGeometry
2. M : Point
3. A : Point
4. B : Point
5. A # B
6. Colinear(A;M;B)
7. MA ≅ MB
8. B-A-M
9. B(BAM)
10. |BM| = |BA| + |BM| ∈ Length
11. |AM| = |BM| ∈ Length
12. 0 + |BM| = |BA| + |BM| ∈ Length
⊢ B(AMB)

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  M  :  Point
3.  A  :  Point
4.  B  :  Point
5.  A  \#  B
6.  Colinear(A;M;B)
7.  MA  \mcong{}  MB
8.  B-A-M
9.  B(BAM)
10.  |BM|  =  |BA|  +  |BM|
11.  |AM|  =  |BM|
12.  |BM|  +  X  =  |BA|  +  |BM|
\mvdash{}  B(AMB)


By

---

Latex:
(Fold  `geo-zero-length`  (-1)  THEN  (RW  (AddrC  [2]  (LemmaC  `geo-add-length-comm`))  (-1)  THENA  Auto))

---

Home Index