---

Step * of Lemma rv-five-segment-lemma

No Annotations
∀n:ℕ. ∀A,B,C,D:ℝ^n. ∀t:ℝ.
  ((t ∈ (r0, r1))
  ⇒ req-vec(n;B;t*A + r1 - t*C)
  ⇒ let a = d(D;B) in
      let b = d(A;D) in
      let c = d(B;C) in
      let d = d(A;B) in
      let x = d(D;C) in
      let s = (t/t - r1) in
      x^2 = (c^2 + a^2 + (s * (b^2 - d^2 + a^2))))
BY
{ (Auto THEN Reduce -2 THEN RepUR ``let`` 0 THEN (Assert (t - r1) < r0 BY (nRAdd ⌜r1⌝ 0⋅ THEN Auto))) }

1
1. n : ℕ
2. A : ℝ^n
3. B : ℝ^n
4. C : ℝ^n
5. D : ℝ^n
6. t : ℝ
7. (r0 < t) ∧ (t < r1)
8. req-vec(n;B;t*A + r1 - t*C)
9. (t - r1) < r0
⊢ d(D;C)^2 = (d(B;C)^2 + d(D;B)^2 + ((t/t - r1) * (d(A;D)^2 - d(A;B)^2 + d(D;B)^2)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}A,B,C,D:\mBbbR{}\^{}n.  \mforall{}t:\mBbbR{}.
    ((t  \mmember{}  (r0,  r1))
    {}\mRightarrow{}  req-vec(n;B;t*A  +  r1  -  t*C)
    {}\mRightarrow{}  let  a  =  d(D;B)  in
            let  b  =  d(A;D)  in
            let  c  =  d(B;C)  in
            let  d  =  d(A;B)  in
            let  x  =  d(D;C)  in
            let  s  =  (t/t  -  r1)  in
            x\^{}2  =  (c\^{}2  +  a\^{}2  +  (s  *  (b\^{}2  -  d\^{}2  +  a\^{}2))))


By

---

Latex:
(Auto  THEN  Reduce  -2  THEN  RepUR  ``let``  0  THEN  (Assert  (t  -  r1)  <  r0  BY  (nRAdd  \mkleeneopen{}r1\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index