---

Step * 1 of Lemma qlog-lemma

.....assertion..... 
1. e : {e:ℚ| 0 < e} 
2. q : {q:ℚ| (e ≤ q) ∧ q < 1} 
⊢ ∀[d:ℕ]
    ∀k:ℕ+. ∀r:{r:ℚ| (e ≤ r) ∧ (r = q ↑ k ∈ ℚ) ∧ q ↑ d * r < e} .
      {nz:ℕ × ℚ| let n,z = nz in (z = q ↑ n ∈ ℚ) ∧ (e ≤ z) ∧ z * z < e} 
BY
{ (UniformCompNatInd
   THEN Auto
   THEN (Evaluate ⌜m = (2 * k) ∈ ℤ⌝⋅ THENA Auto)
   THEN (Evaluate ⌜rr = (r * r) ∈ ℚ⌝⋅ THENA Auto)
   THEN (Decide rr < e THENA Auto)) }

1
1. e : {e:ℚ| 0 < e} 
2. q : {q:ℚ| (e ≤ q) ∧ q < 1} 
3. [n] : ℕ
4. ∀[m:ℕn]
     ∀k:ℕ+. ∀r:{r:ℚ| (e ≤ r) ∧ (r = q ↑ k ∈ ℚ) ∧ q ↑ m * r < e} .
       {nz:ℕ × ℚ| let n,z = nz in (z = q ↑ n ∈ ℚ) ∧ (e ≤ z) ∧ z * z < e} 
5. k : ℕ+
6. r : {r:ℚ| (e ≤ r) ∧ (r = q ↑ k ∈ ℚ) ∧ q ↑ n * r < e} 
7. m : ℤ
8. m = (2 * k) ∈ ℤ
9. rr : ℚ
10. rr = (r * r) ∈ ℚ
11. rr < e
⊢ {nz:ℕ × ℚ| let n,z = nz in (z = q ↑ n ∈ ℚ) ∧ (e ≤ z) ∧ z * z < e} 

2
1. e : {e:ℚ| 0 < e} 
2. q : {q:ℚ| (e ≤ q) ∧ q < 1} 
3. [n] : ℕ
4. ∀[m:ℕn]
     ∀k:ℕ+. ∀r:{r:ℚ| (e ≤ r) ∧ (r = q ↑ k ∈ ℚ) ∧ q ↑ m * r < e} .
       {nz:ℕ × ℚ| let n,z = nz in (z = q ↑ n ∈ ℚ) ∧ (e ≤ z) ∧ z * z < e} 
5. k : ℕ+
6. r : {r:ℚ| (e ≤ r) ∧ (r = q ↑ k ∈ ℚ) ∧ q ↑ n * r < e} 
7. m : ℤ
8. m = (2 * k) ∈ ℤ
9. rr : ℚ
10. rr = (r * r) ∈ ℚ
11. ¬rr < e
⊢ {nz:ℕ × ℚ| let n,z = nz in (z = q ↑ n ∈ ℚ) ∧ (e ≤ z) ∧ z * z < e} 

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
2.  q  :  \{q:\mBbbQ{}|  (e  \mleq{}  q)  \mwedge{}  q  <  1\} 
\mvdash{}  \mforall{}[d:\mBbbN{}]
        \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}r:\{r:\mBbbQ{}|  (e  \mleq{}  r)  \mwedge{}  (r  =  q  \muparrow{}  k)  \mwedge{}  q  \muparrow{}  d  *  r  <  e\}  .
            \{nz:\mBbbN{}  \mtimes{}  \mBbbQ{}|  let  n,z  =  nz  in  (z  =  q  \muparrow{}  n)  \mwedge{}  (e  \mleq{}  z)  \mwedge{}  z  *  z  <  e\} 


By

---

Latex:
(UniformCompNatInd
  THEN  Auto
  THEN  (Evaluate  \mkleeneopen{}m  =  (2  *  k)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}rr  =  (r  *  r)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Decide  rr  <  e  THENA  Auto))

---

Home Index