---

Step * 1 1 2 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 ∈ ℤ
10. (5 * 10^n - 1) = N2 ∈ ℤ
⊢ (2 * N2) = N ∈ ℤ
BY
{ ((Assert (2 * (N ÷ 2)) = (2 * N2) ∈ ℤ BY Auto) THEN (RWO "div_rem_sum2" (-1) 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 ∈ ℤ
11. (N - N rem 2) = (2 * N2) ∈ ℤ
⊢ (2 * N2) = N ∈ ℤ

---

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


By

---

Latex:
((Assert  (2  *  (N  \mdiv{}  2))  =  (2  *  N2)  BY  Auto)  THEN  (RWO  "div\_rem\_sum2"  (-1)  THENA  Auto))

---

Home Index