---

Step * of Lemma ravg-dist-when-rleq

∀[x,y:ℝ].  ((ravg(x;y) - x) = ((r1/r(2)) * (y - x))) ∧ ((y - ravg(x;y)) = ((r1/r(2)) * (y - x))) supposing x ≤ y
BY
{ (Auto THEN InstLemma `ravg-dist` [⌜x⌝;⌜y⌝]⋅ THEN Auto THEN (InstLemma `ravg-weak-between` [⌜x⌝;⌜y⌝]⋅ THENA Auto)) }

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

2
1. x : ℝ
2. y : ℝ
3. x ≤ y
4. (ravg(x;y) - x) = ((r1/r(2)) * (y - x))
5. |ravg(x;y) - x| = ((r1/r(2)) * |y - x|)
6. |ravg(x;y) - y| = ((r1/r(2)) * |y - x|)
7. (x ≤ ravg(x;y)) ∧ (ravg(x;y) ≤ y)
⊢ (y - ravg(x;y)) = ((r1/r(2)) * (y - x))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  InstLemma  `ravg-dist`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `ravg-weak-between`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index