---

Step * of Lemma int-rdiv-int-rmul

No Annotations
∀[k:ℤ-o]. ∀[a:ℝ].  (k * (a)/k = a)
BY
{ ((Auto THEN (BLemma `req-iff-bdd-diff` THENA Auto))
   THEN With ⌜4⌝ (D 0)⋅
   THEN Auto
   THEN D 2
   THEN Unhide
   THEN Auto
   THEN ((RepUR ``int-rmul int-rdiv`` 0⋅ THEN RepeatFor 2 (((CallByValueReduce 0 THENA Auto) THEN Reduce 0)))
         THEN Repeat (AutoSplit)
         THEN (Mul ⌜|k|⌝ 0⋅ THENA Auto)
         THEN (RWO "absval_mul<" 0 THENA Auto)
         THEN (RWO "left_mul_subtract_distrib" 0⋅ THENA Auto)
         THEN (Subst' k * (-((a ((-k) * n)) ÷ k)) ~ -(k * ((a ((-k) * n)) ÷ k)) 0 THENA Auto)
         THEN (RWO "div_rem_sum2" 0 THENA Auto))⋅) }

1
1. k : ℤ-o
2. a : ℕ+ ⟶ ℤ
3. regular-seq(a)
4. n : ℕ+
5. k < 0
⊢ |(-((a ((-k) * n)) - a ((-k) * n) rem k)) - k * (a n)| ≤ (|k| * 4)

2
1. k : ℤ-o
2. ¬k < 0
3. a : ℕ+ ⟶ ℤ
4. regular-seq(a)
5. n : ℕ+
6. 0 < k
⊢ |(a (k * n)) - a (k * n) rem k - k * (a n)| ≤ (|k| * 4)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbZ{}\msupminus{}\msupzero{}].  \mforall{}[a:\mBbbR{}].    (k  *  (a)/k  =  a)


By

---

Latex:
((Auto  THEN  (BLemma  `req-iff-bdd-diff`  THENA  Auto))
  THEN  With  \mkleeneopen{}4\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  D  2
  THEN  Unhide
  THEN  Auto
  THEN  ((RepUR  ``int-rmul  int-rdiv``  0\mcdot{}
                THEN  RepeatFor  2  (((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0))
                )
              THEN  Repeat  (AutoSplit)
              THEN  (Mul  \mkleeneopen{}|k|\mkleeneclose{}  0\mcdot{}  THENA  Auto)
              THEN  (RWO  "absval\_mul<"  0  THENA  Auto)
              THEN  (RWO  "left\_mul\_subtract\_distrib"  0\mcdot{}  THENA  Auto)
              THEN  (Subst'  k  *  (-((a  ((-k)  *  n))  \mdiv{}  k))  \msim{}  -(k  *  ((a  ((-k)  *  n))  \mdiv{}  k))  0  THENA  Auto)
              THEN  (RWO  "div\_rem\_sum2"  0  THENA  Auto))\mcdot{})

---

Home Index