---

Step * of Lemma rmul-rmin

∀[x,y,z:ℝ].  ((r0 ≤ z) ⇒ ((z * rmin(x;y)) = rmin(z * x;z * y)))
BY
{ (Auto
   THEN BLemma `req-iff-bdd-diff`
   THEN Auto
   THEN (RWO "rmul-bdd-diff-reg-seq-mul" 0 THENA (Try (Complete (Auto)) THEN RepUR ``rmin`` 0 THEN Auto))) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. r0 ≤ z
⊢ bdd-diff(reg-seq-mul(z;rmin(x;y));rmin(reg-seq-mul(z;x);reg-seq-mul(z;y)))

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbR{}].    ((r0  \mleq{}  z)  {}\mRightarrow{}  ((z  *  rmin(x;y))  =  rmin(z  *  x;z  *  y)))


By

---

Latex:
(Auto
  THEN  BLemma  `req-iff-bdd-diff`
  THEN  Auto
  THEN  (RWO  "rmul-bdd-diff-reg-seq-mul"  0
              THENA  (Try  (Complete  (Auto))  THEN  RepUR  ``rmin``  0  THEN  Auto)
              ))

---

Home Index