---

Step * 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))) - ((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))
BY
{ ((Subst' (((2 * k) * m) * (x ((2 * k) * n))) - ((2 * k) * n) * (x ((2 * k) * m)) ~ (2 * k)
    * ((m * (x ((2 * k) * n))) - n * (x ((2 * k) * m))) -1
    THENA Auto
    )
   THEN (RWO "absval_mul" (-1) THENA Auto)
   THEN (Subst' |2 * k| ~ 2 * k -1 THENA Auto)
   THEN (Assert |(m * (x ((2 * k) * n))) - n * (x ((2 * k) * m))| ≤ (2 * (n + m)) BY
               (Mul ⌜2 * k⌝ 0⋅ THEN 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))
⊢ (|(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)
14.  |(((2  *  k)  *  m)  *  (x  ((2  *  k)  *  n)))  -  ((2  *  k)  *  n)  *  (x  ((2  *  k)  *  m))|  \mleq{}  ((2  *  1)
        *  (((2  *  k)  *  n)  +  ((2  *  k)  *  m)))
\mvdash{}  (|(m  *  (x  ((2  *  k)  *  n)))  -  n  *  (x  ((2  *  k)  *  m))|  +  |(n  *  v1)  -  m  *  v|)  \mleq{}  (((2  *  k)  +  1)
    *  (n  +  m))


By

---

Latex:
((Subst'  (((2  *  k)  *  m)  *  (x  ((2  *  k)  *  n)))  -  ((2  *  k)  *  n)  *  (x  ((2  *  k)  *  m))  \msim{}  (2  *  k)
    *  ((m  *  (x  ((2  *  k)  *  n)))  -  n  *  (x  ((2  *  k)  *  m)))  -1
    THENA  Auto
    )
  THEN  (RWO  "absval\_mul"  (-1)  THENA  Auto)
  THEN  (Subst'  |2  *  k|  \msim{}  2  *  k  -1  THENA  Auto)
  THEN  (Assert  |(m  *  (x  ((2  *  k)  *  n)))  -  n  *  (x  ((2  *  k)  *  m))|  \mleq{}  (2  *  (n  +  m))  BY
                          (Mul  \mkleeneopen{}2  *  k\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index