---

Step * 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
⊢ D - C^2 = (B - C^2 + D - B^2 + ((t/t - r1) * (A - D^2 - A - B^2 + D - B^2)))
BY
{ (((Assert D - C ≡ D - B + B - C BY (RealVecEqual THEN Auto)) THEN (RWO  "-1" 0 THENA Auto))
   THEN (Assert A - D ≡ A - B - D - B BY
               (RealVecEqual THEN Auto))
   THEN (RWO  "-1" 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
⊢ 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)))

---

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
\mvdash{}  D  -  C\^{}2  =  (B  -  C\^{}2  +  D  -  B\^{}2  +  ((t/t  -  r1)  *  (A  -  D\^{}2  -  A  -  B\^{}2  +  D  -  B\^{}2)))


By

---

Latex:
(((Assert  D  -  C  \mequiv{}  D  -  B  +  B  -  C  BY  (RealVecEqual  THEN  Auto))  THEN  (RWO    "-1"  0  THENA  Auto))
  THEN  (Assert  A  -  D  \mequiv{}  A  -  B  -  D  -  B  BY
                          (RealVecEqual  THEN  Auto))
  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index