---

Step * of Lemma ip-five-segment-lemma

No Annotations
∀[rv:InnerProductSpace]. ∀[A,B,C,D:Point(rv)]. ∀[t:ℝ].
  ((t ∈ (r0, r1))
  ⇒ B ≡ t*A + r1 - t*C
  ⇒ let a = ||D - B|| in
      let b = ||A - D|| in
      let c = ||B - C|| in
      let d = ||A - B|| in
      let x = ||D - C|| in
      let s = (t/t - r1) in
      x^2 = (c^2 + a^2 + (s * (b^2 - d^2 + a^2))))
BY
{ (RepUR ``let`` 0
   THEN Auto
   THEN (Assert (t - r1) < r0 BY
               (nRAdd ⌜r1⌝ 0⋅ THEN Auto))
   THEN Auto
   THEN (RWO  "rv-norm-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
⊢ D - C^2 = (B - C^2 + D - B^2 + ((t/t - r1) * (A - D^2 - A - B^2 + D - B^2)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[rv:InnerProductSpace].  \mforall{}[A,B,C,D:Point(rv)].  \mforall{}[t:\mBbbR{}].
    ((t  \mmember{}  (r0,  r1))
    {}\mRightarrow{}  B  \mequiv{}  t*A  +  r1  -  t*C
    {}\mRightarrow{}  let  a  =  ||D  -  B||  in
            let  b  =  ||A  -  D||  in
            let  c  =  ||B  -  C||  in
            let  d  =  ||A  -  B||  in
            let  x  =  ||D  -  C||  in
            let  s  =  (t/t  -  r1)  in
            x\^{}2  =  (c\^{}2  +  a\^{}2  +  (s  *  (b\^{}2  -  d\^{}2  +  a\^{}2))))


By

---

Latex:
(RepUR  ``let``  0
  THEN  Auto
  THEN  (Assert  (t  -  r1)  <  r0  BY
                          (nRAdd  \mkleeneopen{}r1\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  Auto
  THEN  (RWO    "rv-norm-squared"  0  THENA  Auto))

---

Home Index