---

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


1. rv : InnerProductSpace
2. A : Point(rv)
3. B : Point(rv)
4. C : Point(rv)
5. D : Point(rv)
6. t : ℝ
7. r0 < t
8. t < r1
9. B ≡ t*A + r1 - t*C
10. (t - r1) < r0
11. D - C ≡ D - B + B - C
12. A - D ≡ A - B - D - B
⊢ D - B + B - C^2 = (B - C^2 + D - B^2 + ((t/t - r1) * (A - B - D - B^2 - A - B^2 + D - B^2)))
BY
{ ((GenConcl ⌜D - B = BD ∈ Point(rv)⌝⋅ THENA Auto) THEN (GenConcl ⌜B - C = CB ∈ Point(rv)⌝⋅ THENA Auto)) }

1
1. rv : InnerProductSpace
2. A : Point(rv)
3. B : Point(rv)
4. C : Point(rv)
5. D : Point(rv)
6. t : ℝ
7. r0 < t
8. t < r1
9. B ≡ t*A + r1 - t*C
10. (t - r1) < r0
11. D - C ≡ D - B + B - C
12. A - D ≡ A - B - D - B
13. BD : Point(rv)
14. D - B = BD ∈ Point(rv)
15. CB : Point(rv)
16. B - C = CB ∈ Point(rv)
⊢ BD + CB^2 = (CB^2 + BD^2 + ((t/t - r1) * (A - B - BD^2 - A - B^2 + BD^2)))

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  A  :  Point(rv)
3.  B  :  Point(rv)
4.  C  :  Point(rv)
5.  D  :  Point(rv)
6.  t  :  \mBbbR{}
7.  r0  <  t
8.  t  <  r1
9.  B  \mequiv{}  t*A  +  r1  -  t*C
10.  (t  -  r1)  <  r0
11.  D  -  C  \mequiv{}  D  -  B  +  B  -  C
12.  A  -  D  \mequiv{}  A  -  B  -  D  -  B
\mvdash{}  D  -  B  +  B  -  C\^{}2  =  (B  -  C\^{}2  +  D  -  B\^{}2  +  ((t/t  -  r1)  *  (A  -  B  -  D  -  B\^{}2  -  A  -  B\^{}2  +  D  -  B\^{}2)))


By

---

Latex:
((GenConcl  \mkleeneopen{}D  -  B  =  BD\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (GenConcl  \mkleeneopen{}B  -  C  =  CB\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index