---

Step * 1 1 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
⊢ {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
BY
{ ((InstLemma `qlog-lemma-ext` [⌜e⌝;⌜q⌝]⋅ THENA (Auto THEN ∀h:hyp. DSet h  THEN MemTypeCD THEN Auto))
   THEN D (-1)
   THEN D -2
   THEN Reduce (-1)
   THEN CaseNat 1 `n1')⋅ }

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. [%7] : (n2 = q ↑ n1 ∈ ℚ) ∧ (e ≤ n2) ∧ n2 * n2 < e
9. n1 = 1 ∈ ℤ
⊢ {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 

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. [%7] : (n2 = q ↑ n1 ∈ ℚ) ∧ (e ≤ n2) ∧ n2 * n2 < e
9. ¬(n1 = 1 ∈ ℤ)
⊢ {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < 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
\mvdash{}  \{n:\mBbbN{}\msupplus{}|  (e  \mleq{}  q  \muparrow{}  n  -  1)  \mwedge{}  q  \muparrow{}  n  <  e\} 


By

---

Latex:
((InstLemma  `qlog-lemma-ext`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  \mforall{}h:hyp.  DSet  h    THEN  MemTypeCD  THEN  Auto))
  THEN  D  (-1)
  THEN  D  -2
  THEN  Reduce  (-1)
  THEN  CaseNat  1  `n1')\mcdot{}

---

Home Index