---

Step * 1 1 1 1 of Lemma accelerate-real-strong-regular


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

1
1. k : ℕ+
2. x : ℕ+ ⟶ ℤ
3. ∀n,m:ℕ+.  (|(m * (x n)) - n * (x m)| ≤ ((2 * 1) * (n + m)))
4. n : ℕ+
5. m : ℕ+
6. 2 * k ~ |2 * k|
7. ∀a:ℤ. (|a rem 2 * k| ≤ ((2 * k) - 1))
8. v : ℤ
9. (x ((2 * k) * n) rem 2 * k) = v ∈ ℤ
10. |v| ≤ ((2 * k) - 1)
11. v1 : ℤ
12. (x ((2 * k) * m) rem 2 * k) = v1 ∈ ℤ
13. |v1| ≤ ((2 * k) - 1)
14. ((2 * k) * |(m * (x ((2 * k) * n))) - n * (x ((2 * k) * m))|) ≤ ((2 * 1) * (((2 * k) * n) + ((2 * k) * m)))
15. |(m * (x ((2 * k) * n))) - n * (x ((2 * k) * m))| ≤ (2 * (n + m))
⊢ ((2 * (n + m)) + (n * |v1|) + (m * |v|)) ≤ (((2 * k) + 1) * (n + m))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  ((2  *  1)  *  (n  +  m)))
4.  n  :  \mBbbN{}\msupplus{}
5.  m  :  \mBbbN{}\msupplus{}
6.  2  *  k  \msim{}  |2  *  k|
7.  \mforall{}a:\mBbbZ{}.  (|a  rem  2  *  k|  \mleq{}  ((2  *  k)  -  1))
8.  v  :  \mBbbZ{}
9.  (x  ((2  *  k)  *  n)  rem  2  *  k)  =  v
10.  |v|  \mleq{}  ((2  *  k)  -  1)
11.  v1  :  \mBbbZ{}
12.  (x  ((2  *  k)  *  m)  rem  2  *  k)  =  v1
13.  |v1|  \mleq{}  ((2  *  k)  -  1)
14.  ((2  *  k)  *  |(m  *  (x  ((2  *  k)  *  n)))  -  n  *  (x  ((2  *  k)  *  m))|)  \mleq{}  ((2  *  1)
        *  (((2  *  k)  *  n)  +  ((2  *  k)  *  m)))
15.  |(m  *  (x  ((2  *  k)  *  n)))  -  n  *  (x  ((2  *  k)  *  m))|  \mleq{}  (2  *  (n  +  m))
\mvdash{}  (|(m  *  (x  ((2  *  k)  *  n)))  -  n  *  (x  ((2  *  k)  *  m))|  +  |(n  *  v1)  -  m  *  v|)  \mleq{}  (((2  *  k)  +  1)
    *  (n  +  m))


By

---

Latex:
((RWO    "-1"  0  THENA  Auto)
  THEN  (RWO    "int-triangle-inequality2"  0  THENA  Auto)
  THEN  (RWO    "absval\_mul"  0  THENA  Auto)
  THEN  (Subst'  |n|  \msim{}  n  0  THENA  Auto)
  THEN  (Subst'  |m|  \msim{}  m  0  THENA  Auto))

---

Home Index