---

Step * 1 1 2 2 2 2 of Lemma qlog-exists


1. q : {q:ℚ| (0 ≤ q) ∧ q < 1} 
2. [n] : ℕ
3. ∀[m:ℕn]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ m < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
4. e : {e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ n < e} 
5. e ≤ q
6. n1 : ℕ
7. n2 : ℚ
8. [%7] : (n2 = q ↑ n1 ∈ ℚ) ∧ (e ≤ n2) ∧ n2 * n2 < e
9. ¬(n1 = 1 ∈ ℤ)
10. ¬(n1 = 0 ∈ ℤ)
11. 0 < n2
12. 0 ≤ (n - n1)
13. {n:ℕ+| ((e/n2) ≤ q ↑ n - 1) ∧ q ↑ n < (e/n2)} 
⊢ {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
BY
{ (RenameVar `m' (-1) THEN D -1 THEN UseWitness ⌜n1 + m⌝⋅ THEN MemTypeCD THEN Auto') }

1
1. q : {q:ℚ| (0 ≤ q) ∧ q < 1} 
2. n : ℕ
3. ∀[m:ℕn]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ m < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
4. e : {e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ n < e} 
5. e ≤ q
6. n1 : ℕ
7. n2 : ℚ
8. n2 = q ↑ n1 ∈ ℚ
9. e ≤ n2
10. n2 * n2 < e
11. ¬(n1 = 1 ∈ ℤ)
12. ¬(n1 = 0 ∈ ℤ)
13. 0 < n2
14. 0 ≤ (n - n1)
15. m : ℕ+
16. (e/n2) ≤ q ↑ m - 1
17. q ↑ m < (e/n2)
⊢ e ≤ q ↑ (n1 + m) - 1

2
1. q : {q:ℚ| (0 ≤ q) ∧ q < 1} 
2. n : ℕ
3. ∀[m:ℕn]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ m < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
4. e : {e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ n < e} 
5. e ≤ q
6. n1 : ℕ
7. n2 : ℚ
8. n2 = q ↑ n1 ∈ ℚ
9. e ≤ n2
10. n2 * n2 < e
11. ¬(n1 = 1 ∈ ℤ)
12. ¬(n1 = 0 ∈ ℤ)
13. 0 < n2
14. 0 ≤ (n - n1)
15. m : ℕ+
16. (e/n2) ≤ q ↑ m - 1
17. q ↑ m < (e/n2)
18. e ≤ q ↑ (n1 + m) - 1
⊢ q ↑ n1 + m < e

---

Latex:

---

Latex:

1.  q  :  \{q:\mBbbQ{}|  (0  \mleq{}  q)  \mwedge{}  q  <  1\} 
2.  [n]  :  \mBbbN{}
3.  \mforall{}[m:\mBbbN{}n].  \mforall{}e:\{e:\mBbbQ{}|  0  <  e  \mwedge{}  (e  \mleq{}  1)  \mwedge{}  q  \muparrow{}  m  <  e\}  .  \{n:\mBbbN{}\msupplus{}|  (e  \mleq{}  q  \muparrow{}  n  -  1)  \mwedge{}  q  \muparrow{}  n  <  e\} 
4.  e  :  \{e:\mBbbQ{}|  0  <  e  \mwedge{}  (e  \mleq{}  1)  \mwedge{}  q  \muparrow{}  n  <  e\} 
5.  e  \mleq{}  q
6.  n1  :  \mBbbN{}
7.  n2  :  \mBbbQ{}
8.  [\%7]  :  (n2  =  q  \muparrow{}  n1)  \mwedge{}  (e  \mleq{}  n2)  \mwedge{}  n2  *  n2  <  e
9.  \mneg{}(n1  =  1)
10.  \mneg{}(n1  =  0)
11.  0  <  n2
12.  0  \mleq{}  (n  -  n1)
13.  \{n:\mBbbN{}\msupplus{}|  ((e/n2)  \mleq{}  q  \muparrow{}  n  -  1)  \mwedge{}  q  \muparrow{}  n  <  (e/n2)\} 
\mvdash{}  \{n:\mBbbN{}\msupplus{}|  (e  \mleq{}  q  \muparrow{}  n  -  1)  \mwedge{}  q  \muparrow{}  n  <  e\} 


By

---

Latex:
(RenameVar  `m'  (-1)  THEN  D  -1  THEN  UseWitness  \mkleeneopen{}n1  +  m\mkleeneclose{}\mcdot{}  THEN  MemTypeCD  THEN  Auto')

---

Home Index