---

Step * 1 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
{ ((Assert (((m * m) * |-r1|) + ((n * n) * |r2|)) ≤ (((2 * n * m) * (n + m)) - (n * n) + (m * m)) BY
          (RWO  "-1 -2" 0 THEN Auto))
   THEN (RWO  "-1" 0 THENA Auto)
   THEN Reduce 0) }

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)
12. (((m * m) * |-r1|) + ((n * n) * |r2|)) ≤ (((2 * n * m) * (n + m)) - (n * n) + (m * m))
⊢ ((((m * |x n|) * 2 * (n + m)) + ((n * |y m|) * 2 * (n + m))) + (((2 * n * m) * (n + m)) - (n * n) + (m * m))) ≤ ((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:
((Assert  (((m  *  m)  *  |-r1|)  +  ((n  *  n)  *  |r2|))  \mleq{}  (((2  *  n  *  m)  *  (n  +  m))  -  (n  *  n)  +  (m  *  m))  BY
                (RWO    "-1  -2"  0  THEN  Auto))
  THEN  (RWO    "-1"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index