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