---

Step * 1 of Lemma alt-int-rdiv_wf

.....aux..... 
1. x : ℝ
2. k : ℕ+
3. k ≠ 1
4. alt-int-rdiv(x;k) ∈ ℕ+ ⟶ ℤ
5. n : ℕ+
6. m : ℕ+
⊢ |k * ((m * [x n ÷ k]) - n * [x m ÷ k])| ≤ (k * 2 * (n + m))
BY
{ ((InstLemma `rounding-div-property` [⌜x n⌝;⌜k⌝]⋅ THENA Auto)
   THEN (InstLemma `rounding-div-property` [⌜x m⌝;⌜k⌝]⋅ THENA Auto)
   THEN Mul ⌜2⌝ 0⋅
   THEN (RWO "absval-diff-symmetry" (-1) THENA Auto)
   THEN (Subst' k * ((m * [x n ÷ k]) - n * [x m ÷ k]) ~ (m * ((k * [x n ÷ k]) - x n))
         + (n * ((x m) - k * [x m ÷ k]))
         + ((m * (x n)) - n * (x m)) 0
         THENA Auto
         )
   THEN (RWW "int-triangle-inequality absval_mul" 0 THENA Auto)) }

1
1. x : ℝ
2. k : ℕ+
3. k ≠ 1
4. alt-int-rdiv(x;k) ∈ ℕ+ ⟶ ℤ
5. n : ℕ+
6. m : ℕ+
7. (2 * |(k * [x n ÷ k]) - x n|) ≤ k
8. (2 * |(x m) - k * [x m ÷ k]|) ≤ k
⊢ (2 * ((|m| * |(k * [x n ÷ k]) - x n|) + (|n| * |(x m) - k * [x m ÷ k]|) + |(m * (x n)) - n * (x m)|)) ≤ (2
  * k
  * 2
  * (n + m))

---

Latex:

---

Latex:
.....aux..... 
1.  x  :  \mBbbR{}
2.  k  :  \mBbbN{}\msupplus{}
3.  k  \mneq{}  1
4.  alt-int-rdiv(x;k)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
5.  n  :  \mBbbN{}\msupplus{}
6.  m  :  \mBbbN{}\msupplus{}
\mvdash{}  |k  *  ((m  *  [x  n  \mdiv{}  k])  -  n  *  [x  m  \mdiv{}  k])|  \mleq{}  (k  *  2  *  (n  +  m))


By

---

Latex:
((InstLemma  `rounding-div-property`  [\mkleeneopen{}x  n\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rounding-div-property`  [\mkleeneopen{}x  m\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Mul  \mkleeneopen{}2\mkleeneclose{}  0\mcdot{}
  THEN  (RWO  "absval-diff-symmetry"  (-1)  THENA  Auto)
  THEN  (Subst'  k  *  ((m  *  [x  n  \mdiv{}  k])  -  n  *  [x  m  \mdiv{}  k])  \msim{}  (m  *  ((k  *  [x  n  \mdiv{}  k])  -  x  n))
              +  (n  *  ((x  m)  -  k  *  [x  m  \mdiv{}  k]))
              +  ((m  *  (x  n))  -  n  *  (x  m))  0
              THENA  Auto
              )
  THEN  (RWW  "int-triangle-inequality  absval\_mul"  0  THENA  Auto))

---

Home Index