---

Step * 2 1 1 of Lemma qlog-exists


1. e : {e:ℚ| 0 < e} 
2. q : {q:ℚ| (0 ≤ q) ∧ q < 1} 
3. ∀[d:ℕ]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ d < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
4. e ≤ q
5. ↓∃N:ℕ+. q ↑ N < e
⊢ {n:ℕ+| ((e ≤ 1) ⇒ (e ≤ q ↑ n - 1)) ∧ q ↑ n < e} 
BY
{ (D (-1) THEN (InstHyp [⌜fst(%3)⌝;⌜e⌝] 3⋅ THENA (D (-1) THEN Reduce 0 THEN Auto)⋅)) }

1
1. e : {e:ℚ| 0 < e} 
2. q : {q:ℚ| (0 ≤ q) ∧ q < 1} 
3. ∀[d:ℕ]. ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1) ∧ q ↑ d < e} . {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
4. e ≤ q
5. [%3] : ∃N:ℕ+. q ↑ N < e
6. {n:ℕ+| (e ≤ q ↑ n - 1) ∧ q ↑ n < e} 
⊢ {n:ℕ+| ((e ≤ 1) ⇒ (e ≤ q ↑ n - 1)) ∧ q ↑ n < e} 

---

Latex:

---

Latex:

1.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
2.  q  :  \{q:\mBbbQ{}|  (0  \mleq{}  q)  \mwedge{}  q  <  1\} 
3.  \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\} 
4.  e  \mleq{}  q
5.  \mdownarrow{}\mexists{}N:\mBbbN{}\msupplus{}.  q  \muparrow{}  N  <  e
\mvdash{}  \{n:\mBbbN{}\msupplus{}|  ((e  \mleq{}  1)  {}\mRightarrow{}  (e  \mleq{}  q  \muparrow{}  n  -  1))  \mwedge{}  q  \muparrow{}  n  <  e\} 


By

---

Latex:
(D  (-1)  THEN  (InstHyp  [\mkleeneopen{}fst(\%3)\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  3\mcdot{}  THENA  (D  (-1)  THEN  Reduce  0  THEN  Auto)\mcdot{}))

---

Home Index