---

Step * 1 of Lemma int-rmul_wf

.....set predicate..... 
1. k : ℤ
2. a : ℕ+ ⟶ ℤ
3. regular-seq(a)
⊢ regular-seq(λn.if (k) < (0)  then -(a ((-k) * n))  else if (0) < (k)  then a (k * n)  else 0)
BY
{ (ParallelLast THEN Reduce 0 THEN Auto THEN Repeat (AutoSplit)) }

1
1. k : ℤ
2. a : ℕ+ ⟶ ℤ
3. ∀n,m:ℕ+.  (|(m * (a n)) - n * (a m)| ≤ ((2 * 1) * (n + m)))
4. n : ℕ+
5. m : ℕ+
6. k < 0
⊢ |(m * (-(a ((-k) * n)))) - n * (-(a ((-k) * m)))| ≤ (2 * (n + m))

2
1. k : ℤ
2. ¬k < 0
3. a : ℕ+ ⟶ ℤ
4. ∀n,m:ℕ+.  (|(m * (a n)) - n * (a m)| ≤ ((2 * 1) * (n + m)))
5. n : ℕ+
6. m : ℕ+
7. 0 < k
⊢ |(m * (a (k * n))) - n * (a (k * m))| ≤ (2 * (n + m))

3
1. k : ℤ
2. ¬0 < k
3. ¬k < 0
4. a : ℕ+ ⟶ ℤ
5. ∀n,m:ℕ+.  (|(m * (a n)) - n * (a m)| ≤ ((2 * 1) * (n + m)))
6. n : ℕ+
7. m : ℕ+
⊢ |(m * 0) - n * 0| ≤ (2 * (n + m))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  k  :  \mBbbZ{}
2.  a  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  regular-seq(a)
\mvdash{}  regular-seq(\mlambda{}n.if  (k)  <  (0)    then  -(a  ((-k)  *  n))    else  if  (0)  <  (k)    then  a  (k  *  n)    else  0)


By

---

Latex:
(ParallelLast  THEN  Reduce  0  THEN  Auto  THEN  Repeat  (AutoSplit))

---

Home Index