Step
*
1
of Lemma
ireal-approx-radd-int
1. x : ℝ
2. y : ℝ
3. j : ℕ
4. M : ℕ+
5. a : ℤ
6. n : ℤ
7. |x - (r(a)/r(2 * M))| ≤ (r(j)/r(M))
⊢ |(x + r(n)) - (r(a + (2 * n * M))/r(2 * M))| ≤ (r(j)/r(M))
BY
{ (Assert (r(a + (2 * n * M))/r(2 * M)) = ((r(a)/r(2 * M)) + r(n)) BY
(nRMul ⌜r(2 * M)⌝ 0 ⋅ THEN Auto)) }
1
1. x : ℝ
2. y : ℝ
3. j : ℕ
4. M : ℕ+
5. a : ℤ
6. n : ℤ
7. |x - (r(a)/r(2 * M))| ≤ (r(j)/r(M))
8. (r(a + (2 * n * M))/r(2 * M)) = ((r(a)/r(2 * M)) + r(n))
⊢ |(x + r(n)) - (r(a + (2 * n * M))/r(2 * M))| ≤ (r(j)/r(M))
Latex:
Latex:
1. x : \mBbbR{}
2. y : \mBbbR{}
3. j : \mBbbN{}
4. M : \mBbbN{}\msupplus{}
5. a : \mBbbZ{}
6. n : \mBbbZ{}
7. |x - (r(a)/r(2 * M))| \mleq{} (r(j)/r(M))
\mvdash{} |(x + r(n)) - (r(a + (2 * n * M))/r(2 * M))| \mleq{} (r(j)/r(M))
By
Latex:
(Assert (r(a + (2 * n * M))/r(2 * M)) = ((r(a)/r(2 * M)) + r(n)) BY
(nRMul \mkleeneopen{}r(2 * M)\mkleeneclose{} 0 \mcdot{} THEN Auto))
Home
Index