---

Step * of Lemma vec-midpoint-dist

∀[n:ℕ]. ∀[a,b:ℝ^n].  (d(a;vec-midpoint(a;b)) = ((r1/r(2)) * d(a;b)))
BY
{ (Auto
   THEN (Assert |(r1/r(2))| = (r1/r(2)) BY
               (BLemma `rabs-of-nonneg`  THEN Auto))
   THEN (RWO "-1<" 0 THENA Auto)
   THEN (RWO "real-vec-dist-dilation<" 0 THENA Auto)
   THEN BLemma `real-vec-dist-equal-iff`
   THEN Auto) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. |(r1/r(2))| = (r1/r(2))
⊢ a - vec-midpoint(a;b)⋅a - vec-midpoint(a;b) = (r1/r(2))*a - (r1/r(2))*b⋅(r1/r(2))*a - (r1/r(2))*b

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbR{}\^{}n].    (d(a;vec-midpoint(a;b))  =  ((r1/r(2))  *  d(a;b)))


By

---

Latex:
(Auto
  THEN  (Assert  |(r1/r(2))|  =  (r1/r(2))  BY
                          (BLemma  `rabs-of-nonneg`    THEN  Auto))
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  (RWO  "real-vec-dist-dilation<"  0  THENA  Auto)
  THEN  BLemma  `real-vec-dist-equal-iff`
  THEN  Auto)

---

Home Index