---

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


1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. i : ℕ+b + 1
5. j : ℕ+b + 1
6. ((((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.  ((((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