---

Step * of Lemma dd_wf

∀d:ℕ+. ∀x:ℝ.
  (d decimal digits of x  ∈ {a:Atom| a = "display-as" ∈ Atom} 
   × {a:Atom| a = "decimal-rational" ∈ Atom} 
   × {z:ℝ| z = x} 
   × {n:ℕ+| n = d ∈ ℤ} 
   × {n:ℤ| |x - (r(n)/r(10^d))| ≤ (r(2)/r(10^d))} )
BY
{ (TACTIC:(Auto THEN Unfold `dd` 0 THEN (GenConcl ⌜10^d = N ∈ ℕ+⌝⋅ THENA (Auto THEN (RWO "exp-fastexp<" 0 THEN Auto)⋅)))
   THEN GenConcl ⌜<"display-as", "decimal-rational", x, d, eval N = N in eval N2 = N ÷ 2 in   x N2>
                  = a
                  ∈ ({a:Atom| a = "display-as" ∈ Atom} 
                    × {a:Atom| a = "decimal-rational" ∈ Atom} 
                    × {z:ℝ| z = x} 
                    × {n:ℕ+| n = d ∈ ℤ} 
                    × {n:ℤ| |x - (r(n)/r(N))| ≤ (r(2)/r(N))} )⌝⋅
   ) }

1
.....wf..... 
1. d : ℕ+
2. x : ℝ
3. N : ℕ+
4. 10^d = N ∈ ℕ+
⊢ <"display-as", "decimal-rational", x, d, eval N = N in eval N2 = N ÷ 2 in   x N2> ∈ {a:Atom| a = "display-as" ∈ Atom} 
  × {a:Atom| a = "decimal-rational" ∈ Atom} 
  × {z:ℝ| z = x} 
  × {n:ℕ+| n = d ∈ ℤ} 
  × {n:ℤ| |x - (r(n)/r(N))| ≤ (r(2)/r(N))} 

2
1. d : ℕ+
2. x : ℝ
3. N : ℕ+
4. 10^d = N ∈ ℕ+
5. a : {a:Atom| a = "display-as" ∈ Atom} 
× {a:Atom| a = "decimal-rational" ∈ Atom} 
× {z:ℝ| z = x} 
× {n:ℕ+| n = d ∈ ℤ} 
× {n:ℤ| |x - (r(n)/r(N))| ≤ (r(2)/r(N))} 
6. <"display-as", "decimal-rational", x, d, eval N = N in eval N2 = N ÷ 2 in   x N2>
= a
∈ ({a:Atom| a = "display-as" ∈ Atom} 
  × {a:Atom| a = "decimal-rational" ∈ Atom} 
  × {z:ℝ| z = x} 
  × {n:ℕ+| n = d ∈ ℤ} 
  × {n:ℤ| |x - (r(n)/r(N))| ≤ (r(2)/r(N))} )
⊢ let answer ⟵ a
  in answer ∈ {a:Atom| a = "display-as" ∈ Atom} 
  × {a:Atom| a = "decimal-rational" ∈ Atom} 
  × {z:ℝ| z = x} 
  × {n:ℕ+| n = d ∈ ℤ} 
  × {n:ℤ| |x - (r(n)/r(N))| ≤ (r(2)/r(N))} 

---

Latex:

---

Latex:
\mforall{}d:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbR{}.
    (d  decimal  digits  of  x    \mmember{}  \{a:Atom|  a  =  "display-as"\} 
      \mtimes{}  \{a:Atom|  a  =  "decimal-rational"\} 
      \mtimes{}  \{z:\mBbbR{}|  z  =  x\} 
      \mtimes{}  \{n:\mBbbN{}\msupplus{}|  n  =  d\} 
      \mtimes{}  \{n:\mBbbZ{}|  |x  -  (r(n)/r(10\^{}d))|  \mleq{}  (r(2)/r(10\^{}d))\}  )


By

---

Latex:
(TACTIC:(Auto
                  THEN  Unfold  `dd`  0
                  THEN  (GenConcl  \mkleeneopen{}10\^{}d  =  N\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  (RWO  "exp-fastexp<"  0  THEN  Auto)\mcdot{})))
  THEN  GenConcl  \mkleeneopen{}<"display-as",  "decimal-rational",  x,  d,  eval  N  =  N  in  eval  N2  =  N  \mdiv{}  2  in      x  N2>  =  \000Ca\mkleeneclose{}\mcdot{}
  )

---

Home Index