---

Step * 1 of Lemma int-rmul-req


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))
BY
{ Repeat (AutoSplit) }

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

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

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

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  a  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  |if  (k)  <  (0)    then  -(a  ((-k)  *  n))    else  if  (0)  <  (k)    then  a  (k  *  n)    else  0  -  ((2  *  n  *  k)
    *  (a  n))  \mdiv{}  2  *  n|  \mleq{}  (2  *  (|k|  +  1))


By

---

Latex:
Repeat  (AutoSplit)

---

Home Index