---

Step * of Lemma rmul-distrib1

∀[x,y,z:ℝ].  ((x * (y + z)) = ((x * y) + (x * z)))
BY
{ (Auto
   THEN (BLemma `req-iff-bdd-diff` THENA Auto)
   THEN (RWO "rmul-bdd-diff-reg-seq-mul" 0 THENA Auto)
   THEN RepUR ``radd`` 0
   THEN (InstLemma `accelerate-bdd-diff` [⌜2⌝;⌜reg-seq-list-add([x * y; x * z])⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN ((InstLemma `accelerate-bdd-diff` [⌜2⌝;⌜reg-seq-list-add([y; z])⌝]⋅ THENA Auto)
         THEN (RWO "reg-seq-mul-comm" 0 THENA Auto)
         THEN (RWO "-1" 0 THENA Auto)
         THEN Thin (-1))⋅) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
⊢ bdd-diff(reg-seq-mul(reg-seq-list-add([y; z]);x);reg-seq-list-add([x * y; x * z]))

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbR{}].    ((x  *  (y  +  z))  =  ((x  *  y)  +  (x  *  z)))


By

---

Latex:
(Auto
  THEN  (BLemma  `req-iff-bdd-diff`  THENA  Auto)
  THEN  (RWO  "rmul-bdd-diff-reg-seq-mul"  0  THENA  Auto)
  THEN  RepUR  ``radd``  0
  THEN  (InstLemma  `accelerate-bdd-diff`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}reg-seq-list-add([x  *  y;  x  *  z])\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  ((InstLemma  `accelerate-bdd-diff`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}reg-seq-list-add([y;  z])\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (RWO  "reg-seq-mul-comm"  0  THENA  Auto)
              THEN  (RWO  "-1"  0  THENA  Auto)
              THEN  Thin  (-1))\mcdot{})

---

Home Index