---

Step * 1 1 2 of Lemma ddr_wf


1. x : ℝ
2. n : ℕ+
3. |x - (x within 1/5 * 10^n - 1)| ≤ (r1/r(5 * 10^n - 1))
4. N : {10...}
5. 10^n = N ∈ {10...}
6. N2 : {5...}
7. (N ÷ 2) = N2 ∈ {5...}
8. a : ℤ
9. (x N2) = a ∈ ℤ
10. (5 * 10^n - 1) = N2 ∈ ℤ
⊢ |x - r(a/N)| ≤ (r1/r(5 * 10^n - 1))
BY
{ (RWO "3<" 0⋅ THENA Auto) }

1
1. x : ℝ
2. n : ℕ+
3. |x - (x within 1/5 * 10^n - 1)| ≤ (r1/r(5 * 10^n - 1))
4. N : {10...}
5. 10^n = N ∈ {10...}
6. N2 : {5...}
7. (N ÷ 2) = N2 ∈ {5...}
8. a : ℤ
9. (x N2) = a ∈ ℤ
10. (5 * 10^n - 1) = N2 ∈ ℤ
⊢ |x - r(a/N)| ≤ |x - (x within 1/5 * 10^n - 1)|

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  |x  -  (x  within  1/5  *  10\^{}n  -  1)|  \mleq{}  (r1/r(5  *  10\^{}n  -  1))
4.  N  :  \{10...\}
5.  10\^{}n  =  N
6.  N2  :  \{5...\}
7.  (N  \mdiv{}  2)  =  N2
8.  a  :  \mBbbZ{}
9.  (x  N2)  =  a
10.  (5  *  10\^{}n  -  1)  =  N2
\mvdash{}  |x  -  r(a/N)|  \mleq{}  (r1/r(5  *  10\^{}n  -  1))


By

---

Latex:
(RWO  "3<"  0\mcdot{}  THENA  Auto)

---

Home Index