---

Step * 1 of Lemma ddr_wf


1. x : ℝ
2. n : ℕ+
3. |x - (x within 1/5 * 10^n - 1)| ≤ (r1/r(5 * 10^n - 1))
⊢ ddr(x;n) ∈ {y:ℝ| |x - y| ≤ (r1/r(5 * 10^n - 1))} 
BY
{ (Unfold `ddr` 0
   THEN MemTypeCD
   THEN (RWW "exp-fastexp<" 0 THENA Auto)
   THEN (GenConcl ⌜10^n = N ∈ {10...}⌝⋅
         THENA (Auto THEN (Assert 1 ≤ 10^n - 1 BY Auto) THEN Mul ⌜10⌝ (-1)⋅ THEN RWO "exp_step" 0 THEN Auto)
         )
   THEN (CallByValueReduce 0 THENA (D -2 THEN All Thin THEN Auto))
   THEN (GenConcl ⌜(N ÷ 2) = N2 ∈ {5...}⌝⋅
         THENA (Auto
                THEN (InstLemma `div_rem_sum` [⌜N⌝;⌜2⌝]⋅ THENA Auto)
                THEN InstLemma `rem_bounds_1` [⌜N⌝;⌜2⌝]⋅
                THEN Auto)
         )
   THEN (CallByValueReduce 0 THENA (D -2 THEN All Thin THEN Auto))
   THEN (GenConcl ⌜(x N2) = a ∈ ℤ⌝⋅ THENA Auto)
   THEN CallByValueReduce 0
   THEN 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 ∈ ℤ
⊢ |x - r(a/N)| ≤ (r1/r(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))
\mvdash{}  ddr(x;n)  \mmember{}  \{y:\mBbbR{}|  |x  -  y|  \mleq{}  (r1/r(5  *  10\^{}n  -  1))\} 


By

---

Latex:
(Unfold  `ddr`  0
  THEN  MemTypeCD
  THEN  (RWW  "exp-fastexp<"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}10\^{}n  =  N\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  (Assert  1  \mleq{}  10\^{}n  -  1  BY
                                                    Auto)
                            THEN  Mul  \mkleeneopen{}10\mkleeneclose{}  (-1)\mcdot{}
                            THEN  RWO  "exp\_step"  0
                            THEN  Auto)
              )
  THEN  (CallByValueReduce  0  THENA  (D  -2  THEN  All  Thin  THEN  Auto))
  THEN  (GenConcl  \mkleeneopen{}(N  \mdiv{}  2)  =  N2\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}N\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}N\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}
                            THEN  Auto)
              )
  THEN  (CallByValueReduce  0  THENA  (D  -2  THEN  All  Thin  THEN  Auto))
  THEN  (GenConcl  \mkleeneopen{}(x  N2)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  CallByValueReduce  0
  THEN  Auto)

---

Home Index