---

Step * of Lemma vec-midpoint-symmetry

∀[n:ℕ]. ∀[a,b:ℝ^n].  req-vec(n;vec-midpoint(b;a);vec-midpoint(a;b))
BY
{ (Auto
   THEN RepUR ``req-vec vec-midpoint real-vec-mul real-vec-sub real-vec-add`` 0
   THEN Auto
   THEN BLemma `rmul_functionality`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbR{}\^{}n].    req-vec(n;vec-midpoint(b;a);vec-midpoint(a;b))


By

---

Latex:
(Auto
  THEN  RepUR  ``req-vec  vec-midpoint  real-vec-mul  real-vec-sub  real-vec-add``  0
  THEN  Auto
  THEN  BLemma  `rmul\_functionality`
  THEN  Auto)

---

Home Index