---

Step * 1 1 2 1 1 1 1 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 ∈ ℤ
11. (N - N rem 2) = (2 * N2) ∈ ℤ
⊢ (2 * N2) = N ∈ ℤ
BY
{ ((Subst' N rem 2 ~ 0 -1 THEN Auto) THEN Eliminate ⌜N⌝⋅ THEN All Thin) }

1
1. n : ℕ+
⊢ (10^n rem 2) = 0 ∈ ℤ

---

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
11.  (N  -  N  rem  2)  =  (2  *  N2)
\mvdash{}  (2  *  N2)  =  N


By

---

Latex:
((Subst'  N  rem  2  \msim{}  0  -1  THEN  Auto)  THEN  Eliminate  \mkleeneopen{}N\mkleeneclose{}\mcdot{}  THEN  All  Thin)

---

Home Index