---

Step * 1 1 1 of Lemma ddr_wf

.....assertion..... 
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 ∈ ℤ
⊢ (5 * 10^n - 1) = N2 ∈ ℤ
BY
{ (Eliminate ⌜N2⌝⋅ THEN Eliminate ⌜N⌝⋅ THEN All Thin) }

1
1. n : ℕ+
⊢ (5 * 10^n - 1) = (10^n ÷ 2) ∈ ℤ

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  (5  *  10\^{}n  -  1)  =  N2


By

---

Latex:
(Eliminate  \mkleeneopen{}N2\mkleeneclose{}\mcdot{}  THEN  Eliminate  \mkleeneopen{}N\mkleeneclose{}\mcdot{}  THEN  All  Thin)

---

Home Index