---

Step * 1 1 2 1 1 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. M-B-A
9. B(MBA)
10. |MB| = |MB| + |BA| ∈ Length
11. |MA| = |MB| ∈ Length
12. |MB| + 0 = |MB| + |BA| ∈ Length
⊢ B(AMB)
BY
{ (FLemma `geo-add-length-cancel-left` [-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. M-B-A
9. B(MBA)
10. |MB| = |MB| + |BA| ∈ Length
11. |MA| = |MB| ∈ Length
12. |MB| + 0 = |MB| + |BA| ∈ Length
13. 0 = |BA| ∈ 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.  M-B-A
9.  B(MBA)
10.  |MB|  =  |MB|  +  |BA|
11.  |MA|  =  |MB|
12.  |MB|  +  0  =  |MB|  +  |BA|
\mvdash{}  B(AMB)


By

---

Latex:
(FLemma  `geo-add-length-cancel-left`  [-1]  THENA  Auto)

---

Home Index