---

Step * of Lemma rmul-bdd-diff-reg-seq-mul

∀a,b:ℝ.  bdd-diff(a * b;reg-seq-mul(a;b))
BY
{ (Auto
   THEN (Unfold `rmul` 0 THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto)))
   THEN BLemma `accelerate-bdd-diff`
   THEN ((GenConclTerm ⌜canonical-bound(a)⌝⋅ THENM (Thin (-1) THEN D -1)) THENA Auto)
   THEN ((GenConclTerm ⌜canonical-bound(b)⌝⋅ THENM (Thin (-1) THEN D -1)) THENA Auto)
   THEN Try ((MemTypeCD THEN Auto THEN BLemma `reg-seq-mul-regular` THEN Auto))
   THEN (Assert 2 ≤ imax(v;v1) BY
               (BLemma `imax_ub` THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    bdd-diff(a  *  b;reg-seq-mul(a;b))


By

---

Latex:
(Auto
  THEN  (Unfold  `rmul`  0  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))
  THEN  BLemma  `accelerate-bdd-diff`
  THEN  ((GenConclTerm  \mkleeneopen{}canonical-bound(a)\mkleeneclose{}\mcdot{}  THENM  (Thin  (-1)  THEN  D  -1))  THENA  Auto)
  THEN  ((GenConclTerm  \mkleeneopen{}canonical-bound(b)\mkleeneclose{}\mcdot{}  THENM  (Thin  (-1)  THEN  D  -1))  THENA  Auto)
  THEN  Try  ((MemTypeCD  THEN  Auto  THEN  BLemma  `reg-seq-mul-regular`  THEN  Auto))
  THEN  (Assert  2  \mleq{}  imax(v;v1)  BY
                          (BLemma  `imax\_ub`  THEN  Auto))
  THEN  Auto)

---

Home Index