---

Step * 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)
⊢ |(m * ((x ((2 * k) * n)) - v)) - n * ((x ((2 * k) * m)) - v1)| ≤ (((2 * k) + 1) * (n + m))
BY
{ ((Subst' (m * ((x ((2 * k) * n)) - v)) - n * ((x ((2 * k) * m)) - v1) ~ ((m * (x ((2 * k) * n))) - n
    * (x ((2 * k) * m)))
    + ((n * v1) - m * v) 0
    THENA Auto
    )
   THEN (RWO  "int-triangle-inequality" 0 THEN Auto)
   THEN (InstHyp [⌜(2 * k) * n⌝;⌜(2 * k) * m⌝] 3⋅ 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))) - ((2 * k) * n) * (x ((2 * k) * m))| ≤ ((2 * 1)
    * (((2 * k) * n) + ((2 * k) * m)))
⊢ (|(m * (x ((2 * k) * n))) - n * (x ((2 * k) * 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)
\mvdash{}  |(m  *  ((x  ((2  *  k)  *  n))  -  v))  -  n  *  ((x  ((2  *  k)  *  m))  -  v1)|  \mleq{}  (((2  *  k)  +  1)  *  (n  +  m))


By

---

Latex:
((Subst'  (m  *  ((x  ((2  *  k)  *  n))  -  v))  -  n  *  ((x  ((2  *  k)  *  m))  -  v1)  \msim{}  ((m  *  (x  ((2  *  k)  *  n)))  -  n
    *  (x  ((2  *  k)  *  m)))
    +  ((n  *  v1)  -  m  *  v)  0
    THENA  Auto
    )
  THEN  (RWO    "int-triangle-inequality"  0  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}(2  *  k)  *  n\mkleeneclose{};\mkleeneopen{}(2  *  k)  *  m\mkleeneclose{}]  3\mcdot{}  THENA  Auto))

---

Home Index