---

Step * of Lemma qlog-lemma

No Annotations
∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (e ≤ q) ∧ q < 1} .  {nr:ℕ × ℚ| let n,r = nr in (r = q ↑ n ∈ ℚ) ∧ (e ≤ r) ∧ r * r < e} 
BY
{ (Auto
   THEN Assert ⌜∀[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} ⌝⋅
   ) }

1
.....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} 

2
1. e : {e:ℚ| 0 < e} 
2. q : {q:ℚ| (e ≤ q) ∧ q < 1} 
3. ∀[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} 
⊢ {nr:ℕ × ℚ| let n,r = nr in (r = q ↑ n ∈ ℚ) ∧ (e ≤ r) ∧ r * r < e} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:\{e:\mBbbQ{}|  0  <  e\}  .  \mforall{}q:\{q:\mBbbQ{}|  (e  \mleq{}  q)  \mwedge{}  q  <  1\}  .
    \{nr:\mBbbN{}  \mtimes{}  \mBbbQ{}|  let  n,r  =  nr  in  (r  =  q  \muparrow{}  n)  \mwedge{}  (e  \mleq{}  r)  \mwedge{}  r  *  r  <  e\} 


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}\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\}  \mkleeneclose{}\mcdot{}
  )

---

Home Index