---

Step * 1 1 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
9. (m * 2 * |(k * [x n ÷ k]) - x n|) ≤ (m * k)
10. (n * 2 * |(x m) - k * [x m ÷ k]|) ≤ (n * 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
{ ((Assert |(m * (x n)) - n * (x m)| ≤ (2 * (n + m)) BY (Auto THEN D 1 THEN Unhide THEN Auto)) THEN 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
9. (m * 2 * |(k * [x n ÷ k]) - x n|) ≤ (m * k)
10. (n * 2 * |(x m) - k * [x m ÷ k]|) ≤ (n * k)
11. |(m * (x n)) - n * (x m)| ≤ (2 * (n + m))
⊢ (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
9.  (m  *  2  *  |(k  *  [x  n  \mdiv{}  k])  -  x  n|)  \mleq{}  (m  *  k)
10.  (n  *  2  *  |(x  m)  -  k  *  [x  m  \mdiv{}  k]|)  \mleq{}  (n  *  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:
((Assert  |(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  (2  *  (n  +  m))  BY
                (Auto  THEN  D  1  THEN  Unhide  THEN  Auto))
  THEN  Auto
  )

---

Home Index