---

Step * 2 1 of Lemma regular-int-seq-iff


1. k : ℕ+
2. x : ℕ+ ⟶ ℤ
3. n : ℕ+
4. m : ℕ+
5. ((((x n) - 2 * k) * (2 * k) * m) ≤ (((x m) + (2 * k)) * (2 * k) * n))
∧ ((((x m) - 2 * k) * (2 * k) * n) ≤ (((x n) + (2 * k)) * (2 * k) * m))
⊢ |(m * (x n)) - n * (x m)| ≤ ((2 * k) * (n + m))
BY
{ ((RWO "absval_unfold" 0 THEN Auto) THEN AutoSplit THEN Mul ⌜2 * k⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}\msupplus{}
4.  m  :  \mBbbN{}\msupplus{}
5.  ((((x  n)  -  2  *  k)  *  (2  *  k)  *  m)  \mleq{}  (((x  m)  +  (2  *  k))  *  (2  *  k)  *  n))
\mwedge{}  ((((x  m)  -  2  *  k)  *  (2  *  k)  *  n)  \mleq{}  (((x  n)  +  (2  *  k))  *  (2  *  k)  *  m))
\mvdash{}  |(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  ((2  *  k)  *  (n  +  m))


By

---

Latex:
((RWO  "absval\_unfold"  0  THEN  Auto)  THEN  AutoSplit  THEN  Mul  \mkleeneopen{}2  *  k\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index