---

Step * of Lemma int-rmul-req

∀[k:ℤ]. ∀[a:ℝ].  (k * a = (r(k) * a))
BY
{ TACTIC:TACTIC:(Auto
                 THEN (BLemma `req-iff-bdd-diff` THENA Auto)
                 THEN (TACTIC:RWO "rmul-bdd-diff-reg-seq-mul" 0 THENA Auto)
                 THEN RepUR ``reg-seq-mul int-rmul int-to-real bdd-diff`` 0⋅
                 THEN (CallByValueReduce 0 THENA Auto)
                 THEN Reduce 0
                 THEN With ⌜2 * (|k| + 1)⌝ (D 0)⋅
                 THEN Auto) }

1
1. k : ℤ
2. a : ℝ
3. n : ℕ+@i
⊢ |if (k) < (0)  then -(a ((-k) * n))  else if (0) < (k)  then a (k * n)  else 0 - ((2 * n * k) * (a n)) ÷ 2 * n| ≤ (2
  * (|k| + 1))

---

Latex:

---

Latex:
\mforall{}[k:\mBbbZ{}].  \mforall{}[a:\mBbbR{}].    (k  *  a  =  (r(k)  *  a))


By

---

Latex:
TACTIC:TACTIC:(Auto
                              THEN  (BLemma  `req-iff-bdd-diff`  THENA  Auto)
                              THEN  (TACTIC:RWO  "rmul-bdd-diff-reg-seq-mul"  0  THENA  Auto)
                              THEN  RepUR  ``reg-seq-mul  int-rmul  int-to-real  bdd-diff``  0\mcdot{}
                              THEN  (CallByValueReduce  0  THENA  Auto)
                              THEN  Reduce  0
                              THEN  With  \mkleeneopen{}2  *  (|k|  +  1)\mkleeneclose{}  (D  0)\mcdot{}
                              THEN  Auto)

---

Home Index