---

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


1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. A : Point
7. B : Point
8. C : Point
9. D : Point
10. ||A - C|| = (||A - B|| + ||B - C||)
11. ||a - c|| = (||a - b|| + ||b - c||)
12. a # b
13. t1 : ℝ
14. t1 ∈ (r0, r1)
15. b ≡ t1*a + r1 - t1*c
16. t : ℝ
17. t ∈ (r0, r1)
18. B ≡ t*A + r1 - t*C
19. ab=AB
20. bc=BC
21. ad=AD
22. bd=BD
23. b # c
24. A # B
25. B # C
26. ||d - c||^2 = (||b - c||^2 + ||d - b||^2 + ((t1/t1 - r1) * (||a - d||^2 - ||a - b||^2 + ||d - b||^2)))
27. ||D - C||^2 = (||B - C||^2 + ||D - B||^2 + ((t/t - r1) * (||A - D||^2 - ||A - B||^2 + ||D - B||^2)))
28. (t - r1) < r0
29. (t1 - r1) < r0
⊢ cd=CD
BY
{ (Unfold `ip-congruent` 0 THEN (InstLemma `rnexp-req-iff` [⌜2⌝]⋅ THENA Auto) THEN (RWO  "-1" 0 THENA Auto)) }

1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. A : Point
7. B : Point
8. C : Point
9. D : Point
10. ||A - C|| = (||A - B|| + ||B - C||)
11. ||a - c|| = (||a - b|| + ||b - c||)
12. a # b
13. t1 : ℝ
14. t1 ∈ (r0, r1)
15. b ≡ t1*a + r1 - t1*c
16. t : ℝ
17. t ∈ (r0, r1)
18. B ≡ t*A + r1 - t*C
19. ab=AB
20. bc=BC
21. ad=AD
22. bd=BD
23. b # c
24. A # B
25. B # C
26. ||d - c||^2 = (||b - c||^2 + ||d - b||^2 + ((t1/t1 - r1) * (||a - d||^2 - ||a - b||^2 + ||d - b||^2)))
27. ||D - C||^2 = (||B - C||^2 + ||D - B||^2 + ((t/t - r1) * (||A - D||^2 - ||A - B||^2 + ||D - B||^2)))
28. (t - r1) < r0
29. (t1 - r1) < r0
30. ∀x,y:ℝ.  ((r0 ≤ x) ⇒ (r0 ≤ y) ⇒ (x = y ⇐⇒ x^2 = y^2))
⊢ ||c - d||^2 = ||C - D||^2

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  A  :  Point
7.  B  :  Point
8.  C  :  Point
9.  D  :  Point
10.  ||A  -  C||  =  (||A  -  B||  +  ||B  -  C||)
11.  ||a  -  c||  =  (||a  -  b||  +  ||b  -  c||)
12.  a  \#  b
13.  t1  :  \mBbbR{}
14.  t1  \mmember{}  (r0,  r1)
15.  b  \mequiv{}  t1*a  +  r1  -  t1*c
16.  t  :  \mBbbR{}
17.  t  \mmember{}  (r0,  r1)
18.  B  \mequiv{}  t*A  +  r1  -  t*C
19.  ab=AB
20.  bc=BC
21.  ad=AD
22.  bd=BD
23.  b  \#  c
24.  A  \#  B
25.  B  \#  C
26.  ||d  -  c||\^{}2
=  (||b  -  c||\^{}2  +  ||d  -  b||\^{}2  +  ((t1/t1  -  r1)  *  (||a  -  d||\^{}2  -  ||a  -  b||\^{}2  +  ||d  -  b||\^{}2)))
27.  ||D  -  C||\^{}2
=  (||B  -  C||\^{}2  +  ||D  -  B||\^{}2  +  ((t/t  -  r1)  *  (||A  -  D||\^{}2  -  ||A  -  B||\^{}2  +  ||D  -  B||\^{}2)))
28.  (t  -  r1)  <  r0
29.  (t1  -  r1)  <  r0
\mvdash{}  cd=CD


By

---

Latex:
(Unfold  `ip-congruent`  0
  THEN  (InstLemma  `rnexp-req-iff`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index