---

Step * of Lemma ireal-approx-radd-int

∀[x,y:ℝ]. ∀[j:ℕ]. ∀[M:ℕ+]. ∀[a,n:ℤ].  (j-approx(x;M;a) ⇒ j-approx(x + r(n);M;a + (2 * n * M)))
BY
{ (Auto THEN All (Unfold  `ireal-approx`)) }

1
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))

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].  \mforall{}[j:\mBbbN{}].  \mforall{}[M:\mBbbN{}\msupplus{}].  \mforall{}[a,n:\mBbbZ{}].    (j-approx(x;M;a)  {}\mRightarrow{}  j-approx(x  +  r(n);M;a  +  (2  *  n  *  M)))


By

---

Latex:
(Auto  THEN  All  (Unfold    `ireal-approx`))

---

Home Index