---

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


1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. ∀i,j:ℕ+b + 1.  (|(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j)))
5. n : ℕ+b + 1
6. m : ℕ+b + 1
7. j : ℕ+b + 1
8. seq-max-lower(k;b;x) = j ∈ ℕ+b + 1
9. ((j * (x n)) - n * (x j)) ≤ ((2 * k) * (j - n))
10. ((j * (x m)) - m * (x j)) ≤ ((2 * k) * (j - m))
11. (((x n) - 2 * k) * (2 * k) * j) ≤ (((x j) - 2 * k) * (2 * k) * n)
12. (((x j) - 2 * k) * (2 * k) * n) ≤ (((x n) + (2 * k)) * (2 * k) * j)
13. (((x m) - 2 * k) * (2 * k) * j) ≤ (((x j) - 2 * k) * (2 * k) * m)
⊢ (((x j) - 2 * k) * (2 * k) * m) ≤ (((x m) + (2 * k)) * (2 * k) * j)
BY
{ ((Assert ⌜(((x j) - 2 * k) * m) ≤ (((x m) + (2 * k)) * j)⌝⋅ THENM (Mul ⌜2 * k⌝ (-1)⋅ THEN Auto)) THEN Auto) }

1
.....assertion..... 
1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. ∀i,j:ℕ+b + 1.  (|(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j)))
5. n : ℕ+b + 1
6. m : ℕ+b + 1
7. j : ℕ+b + 1
8. seq-max-lower(k;b;x) = j ∈ ℕ+b + 1
9. ((j * (x n)) - n * (x j)) ≤ ((2 * k) * (j - n))
10. ((j * (x m)) - m * (x j)) ≤ ((2 * k) * (j - m))
11. (((x n) - 2 * k) * (2 * k) * j) ≤ (((x j) - 2 * k) * (2 * k) * n)
12. (((x j) - 2 * k) * (2 * k) * n) ≤ (((x n) + (2 * k)) * (2 * k) * j)
13. (((x m) - 2 * k) * (2 * k) * j) ≤ (((x j) - 2 * k) * (2 * k) * m)
⊢ (((x j) - 2 * k) * m) ≤ (((x m) + (2 * k)) * j)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  b  :  \mBbbN{}\msupplus{}
3.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  \mforall{}i,j:\mBbbN{}\msupplus{}b  +  1.    (|(i  *  (x  j))  -  j  *  (x  i)|  \mleq{}  ((2  *  k)  *  (i  +  j)))
5.  n  :  \mBbbN{}\msupplus{}b  +  1
6.  m  :  \mBbbN{}\msupplus{}b  +  1
7.  j  :  \mBbbN{}\msupplus{}b  +  1
8.  seq-max-lower(k;b;x)  =  j
9.  ((j  *  (x  n))  -  n  *  (x  j))  \mleq{}  ((2  *  k)  *  (j  -  n))
10.  ((j  *  (x  m))  -  m  *  (x  j))  \mleq{}  ((2  *  k)  *  (j  -  m))
11.  (((x  n)  -  2  *  k)  *  (2  *  k)  *  j)  \mleq{}  (((x  j)  -  2  *  k)  *  (2  *  k)  *  n)
12.  (((x  j)  -  2  *  k)  *  (2  *  k)  *  n)  \mleq{}  (((x  n)  +  (2  *  k))  *  (2  *  k)  *  j)
13.  (((x  m)  -  2  *  k)  *  (2  *  k)  *  j)  \mleq{}  (((x  j)  -  2  *  k)  *  (2  *  k)  *  m)
\mvdash{}  (((x  j)  -  2  *  k)  *  (2  *  k)  *  m)  \mleq{}  (((x  m)  +  (2  *  k))  *  (2  *  k)  *  j)


By

---

Latex:
((Assert  \mkleeneopen{}(((x  j)  -  2  *  k)  *  m)  \mleq{}  (((x  m)  +  (2  *  k))  *  j)\mkleeneclose{}\mcdot{}  THENM  (Mul  \mkleeneopen{}2  *  k\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
  THEN  Auto
  )

---

Home Index