---

Step * 1 1 of Lemma alt-int-rdiv_wf


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))
BY
{ ((Subst' |m| ~ m 0 THENA Auto) THEN (Subst' |n| ~ n 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:

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{}
7.  (2  *  |(k  *  [x  n  \mdiv{}  k])  -  x  n|)  \mleq{}  k
8.  (2  *  |(x  m)  -  k  *  [x  m  \mdiv{}  k]|)  \mleq{}  k
\mvdash{}  (2
    *  ((|m|  *  |(k  *  [x  n  \mdiv{}  k])  -  x  n|)
        +  (|n|  *  |(x  m)  -  k  *  [x  m  \mdiv{}  k]|)
        +  |(m  *  (x  n))  -  n  *  (x  m)|))  \mleq{}  (2  *  k  *  2  *  (n  +  m))


By

---

Latex:
((Subst'  |m|  \msim{}  m  0  THENA  Auto)  THEN  (Subst'  |n|  \msim{}  n  0  THENA  Auto))

---

Home Index