---

Step * 1 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
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)))
BY
{ (RWO  "rv-ip-add-squared rv-ip-sub-squared" 0 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^2 + (r(2) * BD ⋅ CB)) + CB^2)
= (CB^2 + BD^2 + ((t/t - r1) * (((A - B^2 - r(2) * A - B ⋅ BD) + BD^2) - ((A^2 - r(2) * A ⋅ B) + 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
13.  BD  :  Point(rv)
14.  D  -  B  =  BD
15.  CB  :  Point(rv)
16.  B  -  C  =  CB
\mvdash{}  BD  +  CB\^{}2  =  (CB\^{}2  +  BD\^{}2  +  ((t/t  -  r1)  *  (A  -  B  -  BD\^{}2  -  A  -  B\^{}2  +  BD\^{}2)))


By

---

Latex:
(RWO    "rv-ip-add-squared  rv-ip-sub-squared"  0  THENA  Auto)

---

Home Index