---

Step * 1 2 1 of Lemma ip-five-segment


1. rv : InnerProductSpace
2. a : Point
3. c : Point
4. d : Point
5. A : Point
6. B : Point
7. C : Point
8. D : Point
9. ||A - C|| = (||A - B|| + ||B - C||)
10. A_B_C
11. ac=AB
12. cc=BC
13. ad=AD
14. cd=BD
⊢ cd=CD
BY
{ ((FLemma `ip-congruent-same` [-3] THENA Auto) THEN RWO "-1" (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point
3.  c  :  Point
4.  d  :  Point
5.  A  :  Point
6.  B  :  Point
7.  C  :  Point
8.  D  :  Point
9.  ||A  -  C||  =  (||A  -  B||  +  ||B  -  C||)
10.  A\_B\_C
11.  ac=AB
12.  cc=BC
13.  ad=AD
14.  cd=BD
\mvdash{}  cd=CD


By

---

Latex:
((FLemma  `ip-congruent-same`  [-3]  THENA  Auto)  THEN  RWO  "-1"  (-2)  THEN  Auto)

---

Home Index