---

Step * 1 1 1 1 1 of Lemma reg-seq-mul-regular-eventually


1. x : ℕ+ ⟶ ℤ
2. y : ℕ+ ⟶ ℤ
3. B : ℕ+
4. b : ℕ+
5. ∀n,m:{b...}.  ((2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 2)))
6. n : {b...}
7. m : {b...}
8. r1 : {r:ℤ| |r| < |2 * n|} 
9. r2 : {r:ℤ| |r| < |2 * m|} 
10. |-r1| ≤ ((2 * n) - 1)
11. |r2| ≤ ((2 * m) - 1)
⊢ ((((m * |x n|) * (2 * 1) * (n + m)) + ((n * |y m|) * (2 * 1) * (n + m))) + ((m * m) * |-r1|) + ((n * n) * |r2|)) 
  ≤ ((|2| * n * m) * (2 * B) * (n + m))
BY
{ (Subst' |2| ~ 2 0 THENA Auto) }

1
1. x : ℕ+ ⟶ ℤ
2. y : ℕ+ ⟶ ℤ
3. B : ℕ+
4. b : ℕ+
5. ∀n,m:{b...}.  ((2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 2)))
6. n : {b...}
7. m : {b...}
8. r1 : {r:ℤ| |r| < |2 * n|} 
9. r2 : {r:ℤ| |r| < |2 * m|} 
10. |-r1| ≤ ((2 * n) - 1)
11. |r2| ≤ ((2 * m) - 1)
⊢ ((((m * |x n|) * (2 * 1) * (n + m)) + ((n * |y m|) * (2 * 1) * (n + m))) + ((m * m) * |-r1|) + ((n * n) * |r2|)) 
  ≤ ((2 * n * m) * (2 * B) * (n + m))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  y  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  B  :  \mBbbN{}\msupplus{}
4.  b  :  \mBbbN{}\msupplus{}
5.  \mforall{}n,m:\{b...\}.    ((2  *  ((m  *  |x  n|)  +  (n  *  |y  m|)))  \mleq{}  ((n  *  m)  *  ((4  *  B)  -  2)))
6.  n  :  \{b...\}
7.  m  :  \{b...\}
8.  r1  :  \{r:\mBbbZ{}|  |r|  <  |2  *  n|\} 
9.  r2  :  \{r:\mBbbZ{}|  |r|  <  |2  *  m|\} 
10.  |-r1|  \mleq{}  ((2  *  n)  -  1)
11.  |r2|  \mleq{}  ((2  *  m)  -  1)
\mvdash{}  ((((m  *  |x  n|)  *  (2  *  1)  *  (n  +  m))  +  ((n  *  |y  m|)  *  (2  *  1)  *  (n  +  m)))
    +  ((m  *  m)  *  |-r1|)
    +  ((n  *  n)  *  |r2|))  \mleq{}  ((|2|  *  n  *  m)  *  (2  *  B)  *  (n  +  m))


By

---

Latex:
(Subst'  |2|  \msim{}  2  0  THENA  Auto)

---

Home Index