---

Step * 1 of Lemma dd_wf

.....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))} 
BY
{ TACTIC:((CallByValueReduce 0 THENA Auto) THEN Assert ⌜N = (2 * (N ÷ 2)) ∈ ℤ⌝⋅) }

1
.....assertion..... 
1. d : ℕ+
2. x : ℝ
3. N : ℕ+
4. 10^d = N ∈ ℕ+
⊢ N = (2 * (N ÷ 2)) ∈ ℤ

2
1. d : ℕ+
2. x : ℝ
3. N : ℕ+
4. 10^d = N ∈ ℕ+
5. N = (2 * (N ÷ 2)) ∈ ℤ
⊢ <"display-as", "decimal-rational", x, d, 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))} 

---

Latex:

---

Latex:
.....wf..... 
1.  d  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbR{}
3.  N  :  \mBbbN{}\msupplus{}
4.  10\^{}d  =  N
\mvdash{}  <"display-as",  "decimal-rational",  x,  d,  eval  N  =  N  in  eval  N2  =  N  \mdiv{}  2  in      x  N2>  \mmember{}  \{a:Atom|  a  =  "\000Cdisplay-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(N))|  \mleq{}  (r(2)/r(N))\} 


By

---

Latex:
TACTIC:((CallByValueReduce  0  THENA  Auto)  THEN  Assert  \mkleeneopen{}N  =  (2  *  (N  \mdiv{}  2))\mkleeneclose{}\mcdot{})

---

Home Index