---

Step * 2 1 1 1 of Lemma regular-upto-iff2


1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. i : ℕ+b + 1
5. j : ℕ+b + 1
6. (r((x i) - 2 * k)/r((2 * k) * i)) ≤ (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x)))
7. (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x))) ≤ (r((x i) + (2 * k))/r((2 * k) * i))
8. (r((x j) - 2 * k)/r((2 * k) * j)) ≤ (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x)))
9. (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x))) ≤ (r((x j) + (2 * k))/r((2 * k) * j))
10. ((((x i) - 2 * k) * (2 * k) * j) ≤ (((x j) + (2 * k)) * (2 * k) * i))
∧ ((((x j) - 2 * k) * (2 * k) * i) ≤ (((x i) + (2 * k)) * (2 * k) * j))
⊢ |(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j))
BY
{ ((RWO "absval_unfold" 0 THEN Auto) THEN AutoSplit THEN Mul ⌜2 * k⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  b  :  \mBbbN{}\msupplus{}
3.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  i  :  \mBbbN{}\msupplus{}b  +  1
5.  j  :  \mBbbN{}\msupplus{}b  +  1
6.  (r((x  i)  -  2  *  k)/r((2  *  k)  *  i))  \mleq{}  (r((x  seq-max-lower(k;b;x))  -  2  *  k)/r((2  *  k)
*  seq-max-lower(k;b;x)))
7.  (r((x  seq-max-lower(k;b;x))  -  2  *  k)/r((2  *  k)  *  seq-max-lower(k;b;x)))  \mleq{}  (r((x  i)
+  (2  *  k))/r((2  *  k)  *  i))
8.  (r((x  j)  -  2  *  k)/r((2  *  k)  *  j))  \mleq{}  (r((x  seq-max-lower(k;b;x))  -  2  *  k)/r((2  *  k)
*  seq-max-lower(k;b;x)))
9.  (r((x  seq-max-lower(k;b;x))  -  2  *  k)/r((2  *  k)  *  seq-max-lower(k;b;x)))  \mleq{}  (r((x  j)
+  (2  *  k))/r((2  *  k)  *  j))
10.  ((((x  i)  -  2  *  k)  *  (2  *  k)  *  j)  \mleq{}  (((x  j)  +  (2  *  k))  *  (2  *  k)  *  i))
\mwedge{}  ((((x  j)  -  2  *  k)  *  (2  *  k)  *  i)  \mleq{}  (((x  i)  +  (2  *  k))  *  (2  *  k)  *  j))
\mvdash{}  |(i  *  (x  j))  -  j  *  (x  i)|  \mleq{}  ((2  *  k)  *  (i  +  j))


By

---

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

---

Home Index