---

Step * 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|
⊢ ((2 * k) * |(m * ((x ((2 * k) * n)) ÷ 2 * k)) - n * ((x ((2 * k) * m)) ÷ 2 * k)|) ≤ (((2 * k) + 1) * (n + m))
BY
{ (HypSubst' (-1) 0
   THEN (RWO "absval_mul<" 0 THENA Auto)
   THEN RevHypSubst' (-1)0
   THEN Auto
   THEN (Subst' (2 * k) * ((m * ((x ((2 * k) * n)) ÷ 2 * k)) - n * ((x ((2 * k) * m)) ÷ 2 * k)) ~ (m
         * (2 * k)
         * ((x ((2 * k) * n)) ÷ 2 * k)) - n * (2 * k) * ((x ((2 * k) * m)) ÷ 2 * k) 0
         THENA Auto
         )
   THEN (RWO  "div_rem_sum2" 0 THENA Auto)
   THEN (Assert ∀a:ℤ. (|a rem 2 * k| ≤ ((2 * k) - 1)) BY
               ((InstLemma `rem_bounds_absval` [⌜2 * k⌝]⋅ THENA Auto)
                THEN (Subst' |2 * k| ~ 2 * k -1 THENA Auto)
                THEN ParallelLast
                THEN Auto))
   THEN (InstHyp [⌜x ((2 * k) * n)⌝] (-1)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerm ⌜x ((2 * k) * n) rem 2 * k⌝⋅
   THEN Auto
   THEN (InstHyp [⌜x ((2 * k) * m)⌝] (-4)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerm ⌜x ((2 * k) * m) rem 2 * k⌝⋅
   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)
⊢ |(m * ((x ((2 * k) * n)) - v)) - n * ((x ((2 * k) * m)) - v1)| ≤ (((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|
\mvdash{}  ((2  *  k)  *  |(m  *  ((x  ((2  *  k)  *  n))  \mdiv{}  2  *  k))  -  n  *  ((x  ((2  *  k)  *  m))  \mdiv{}  2  *  k)|)  \mleq{}  (((2  *  k)  +  1)
    *  (n  +  m))


By

---

Latex:
(HypSubst'  (-1)  0
  THEN  (RWO  "absval\_mul<"  0  THENA  Auto)
  THEN  RevHypSubst'  (-1)0
  THEN  Auto
  THEN  (Subst'  (2  *  k)  *  ((m  *  ((x  ((2  *  k)  *  n))  \mdiv{}  2  *  k))  -  n  *  ((x  ((2  *  k)  *  m))  \mdiv{}  2  *  k))  \msim{}  (m
              *  (2  *  k)
              *  ((x  ((2  *  k)  *  n))  \mdiv{}  2  *  k))  -  n  *  (2  *  k)  *  ((x  ((2  *  k)  *  m))  \mdiv{}  2  *  k)  0
              THENA  Auto
              )
  THEN  (RWO    "div\_rem\_sum2"  0  THENA  Auto)
  THEN  (Assert  \mforall{}a:\mBbbZ{}.  (|a  rem  2  *  k|  \mleq{}  ((2  *  k)  -  1))  BY
                          ((InstLemma  `rem\_bounds\_absval`  [\mkleeneopen{}2  *  k\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (Subst'  |2  *  k|  \msim{}  2  *  k  -1  THENA  Auto)
                            THEN  ParallelLast
                            THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}x  ((2  *  k)  *  n)\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerm  \mkleeneopen{}x  ((2  *  k)  *  n)  rem  2  *  k\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x  ((2  *  k)  *  m)\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerm  \mkleeneopen{}x  ((2  *  k)  *  m)  rem  2  *  k\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index