---

Step * 1 of Lemma qlog-exists

.....assertion..... 
1. e : {e:ℚ| 0 < e} 
2. q : {q:ℚ| (0 ≤ q) ∧ q < 1} 
⊢ ∀[d:ℕ]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ d < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
BY
{ (ThinVar `e' THEN (UniformCompNatInd THEN Auto THEN (Decide e ≤ q THENA 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
⊢ {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)
⊢ {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
2.  q  :  \{q:\mBbbQ{}|  (0  \mleq{}  q)  \mwedge{}  q  <  1\} 
\mvdash{}  \mforall{}[d:\mBbbN{}].  \mforall{}e:\{e:\mBbbQ{}|  0  <  e  \mwedge{}  (e  \mleq{}  1)  \mwedge{}  q  \muparrow{}  d  <  e\}  .  \{n:\mBbbN{}\msupplus{}|  (e  \mleq{}  q  \muparrow{}  n  -  1)  \mwedge{}  q  \muparrow{}  n  <  e\} 


By

---

Latex:
(ThinVar  `e'  THEN  (UniformCompNatInd  THEN  Auto  THEN  (Decide  e  \mleq{}  q  THENA  Auto))\mcdot{})\mcdot{}

---

Home Index