---

Step * 1 1 1 1 1 of Lemma reg_seq_mul-regular-eventually


1. x : ℕ+ ⟶ ℤ
2. ∀n,m:ℕ+.  (|(m * (x n)) - n * (x m)| ≤ ((2 * 1) * (n + m)))
3. y : ℕ+ ⟶ ℤ
4. ∀n,m:ℕ+.  (|(m * (y n)) - n * (y m)| ≤ ((2 * 1) * (n + m)))
5. B : ℕ+
6. b : ℕ+
7. ∀n,m:{b...}.  ((2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 1)))
8. n : {b...}
9. m : {b...}
10. v : ℕ+ ⟶ ℤ
11. reg_seq_mul(x;y) = v ∈ (ℕ+ ⟶ ℤ)
12. ∀n:ℕ+. (|((2 * n) * (v n)) - (x n) * (y n)| ≤ n)
13. ∀m,n:ℕ+.  (|((m * m) * (2 * n) * (v n)) - (m * (x n)) * m * (y n)| ≤ ((m * m) * n))
14. |((m * m) * (2 * n) * (v n)) - (m * (x n)) * m * (y n)| ≤ ((m * m) * n)
15. |((n * (x m)) * n * (y m)) - (n * n) * (2 * m) * (v m)| ≤ ((n * n) * m)
⊢ (((m * m) * n) + ((|m * (x n)| * (2 * 1) * (n + m)) + (|n * (y m)| * (2 * 1) * (n + m))) + ((n * n) * m)) ≤ ((2
                                                                                                               * n
                                                                                                               * m)
  * (2 * B)
  * (n + m))
BY
{ ((RWO "absval_mul" 0 THENA Auto)
   THEN (Subst' |m| ~ m 0 THENA Auto)
   THEN (Subst' |n| ~ n 0 THENA Auto)
   THEN (Subst' (m * |x n|) * (2 * 1) * (n + m) ~ (2 * m * (n + m)) * |x n| 0 THENA Auto)
   THEN (Subst' (n * |y m|) * (2 * 1) * (n + m) ~ (2 * n * (n + m)) * |y m| 0 THENA Auto)) }

1
1. x : ℕ+ ⟶ ℤ
2. ∀n,m:ℕ+.  (|(m * (x n)) - n * (x m)| ≤ ((2 * 1) * (n + m)))
3. y : ℕ+ ⟶ ℤ
4. ∀n,m:ℕ+.  (|(m * (y n)) - n * (y m)| ≤ ((2 * 1) * (n + m)))
5. B : ℕ+
6. b : ℕ+
7. ∀n,m:{b...}.  ((2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 1)))
8. n : {b...}
9. m : {b...}
10. v : ℕ+ ⟶ ℤ
11. reg_seq_mul(x;y) = v ∈ (ℕ+ ⟶ ℤ)
12. ∀n:ℕ+. (|((2 * n) * (v n)) - (x n) * (y n)| ≤ n)
13. ∀m,n:ℕ+.  (|((m * m) * (2 * n) * (v n)) - (m * (x n)) * m * (y n)| ≤ ((m * m) * n))
14. |((m * m) * (2 * n) * (v n)) - (m * (x n)) * m * (y n)| ≤ ((m * m) * n)
15. |((n * (x m)) * n * (y m)) - (n * n) * (2 * m) * (v m)| ≤ ((n * n) * m)
⊢ (((m * m) * n) + (((2 * m * (n + m)) * |x n|) + ((2 * n * (n + m)) * |y m|)) + ((n * n) * m)) ≤ ((2 * n * m)
  * (2 * B)
  * (n + m))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  ((2  *  1)  *  (n  +  m)))
3.  y  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (y  n))  -  n  *  (y  m)|  \mleq{}  ((2  *  1)  *  (n  +  m)))
5.  B  :  \mBbbN{}\msupplus{}
6.  b  :  \mBbbN{}\msupplus{}
7.  \mforall{}n,m:\{b...\}.    ((2  *  ((m  *  |x  n|)  +  (n  *  |y  m|)))  \mleq{}  ((n  *  m)  *  ((4  *  B)  -  1)))
8.  n  :  \{b...\}
9.  m  :  \{b...\}
10.  v  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
11.  reg\_seq\_mul(x;y)  =  v
12.  \mforall{}n:\mBbbN{}\msupplus{}.  (|((2  *  n)  *  (v  n))  -  (x  n)  *  (y  n)|  \mleq{}  n)
13.  \mforall{}m,n:\mBbbN{}\msupplus{}.    (|((m  *  m)  *  (2  *  n)  *  (v  n))  -  (m  *  (x  n))  *  m  *  (y  n)|  \mleq{}  ((m  *  m)  *  n))
14.  |((m  *  m)  *  (2  *  n)  *  (v  n))  -  (m  *  (x  n))  *  m  *  (y  n)|  \mleq{}  ((m  *  m)  *  n)
15.  |((n  *  (x  m))  *  n  *  (y  m))  -  (n  *  n)  *  (2  *  m)  *  (v  m)|  \mleq{}  ((n  *  n)  *  m)
\mvdash{}  (((m  *  m)  *  n)
    +  ((|m  *  (x  n)|  *  (2  *  1)  *  (n  +  m))  +  (|n  *  (y  m)|  *  (2  *  1)  *  (n  +  m)))
    +  ((n  *  n)  *  m))  \mleq{}  ((2  *  n  *  m)  *  (2  *  B)  *  (n  +  m))


By

---

Latex:
((RWO  "absval\_mul"  0  THENA  Auto)
  THEN  (Subst'  |m|  \msim{}  m  0  THENA  Auto)
  THEN  (Subst'  |n|  \msim{}  n  0  THENA  Auto)
  THEN  (Subst'  (m  *  |x  n|)  *  (2  *  1)  *  (n  +  m)  \msim{}  (2  *  m  *  (n  +  m))  *  |x  n|  0  THENA  Auto)
  THEN  (Subst'  (n  *  |y  m|)  *  (2  *  1)  *  (n  +  m)  \msim{}  (2  *  n  *  (n  +  m))  *  |y  m|  0  THENA  Auto))

---

Home Index