---

Step * of Lemma ravg-dist

∀x,y:ℝ.  ((|ravg(x;y) - x| = ((r1/r(2)) * |y - x|)) ∧ (|ravg(x;y) - y| = ((r1/r(2)) * |y - x|)))
BY
{ (Auto
   THEN nRMul ⌜r(2)⌝ 0⋅
   THEN Auto
   THEN (Assert r(2) = |r(2)| BY
               (RWO "rabs-int" 0 THEN Auto))
   THEN (RWO  "-1" 0 THENA Auto)
   THEN (RWO "rabs-rmul<" 0 THENA Auto)
   THEN Unfold `ravg` 0
   THEN nRNorm
   0⋅
   THEN Auto) }

1
1. x : ℝ
2. y : ℝ
3. |ravg(x;y) - x| = ((r1/r(2)) * |y - x|)
4. r(2) = |r(2)|
⊢ |x + -(y)| = |-(x) + y|

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((|ravg(x;y)  -  x|  =  ((r1/r(2))  *  |y  -  x|))  \mwedge{}  (|ravg(x;y)  -  y|  =  ((r1/r(2))  *  |y  -  x|)))


By

---

Latex:
(Auto
  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  (Assert  r(2)  =  |r(2)|  BY
                          (RWO  "rabs-int"  0  THEN  Auto))
  THEN  (RWO    "-1"  0  THENA  Auto)
  THEN  (RWO  "rabs-rmul<"  0  THENA  Auto)
  THEN  Unfold  `ravg`  0
  THEN  nRNorm
  0\mcdot{}
  THEN  Auto)

---

Home Index