Step
*
1
1
of Lemma
qlog-bound
1. e : ℚ
2. q : ℚ
3. 0 < e
4. e ≤ q
5. q < 1
6. a : ℕ+
7. (1/a) < e
⊢ ∃N:ℕ+. q ↑ N < e
BY
{ Assert ⌜∃b:ℕ+. 1 + (1/b) < (1/q)⌝⋅ }
1
.....assertion.....
1. e : ℚ
2. q : ℚ
3. 0 < e
4. e ≤ q
5. q < 1
6. a : ℕ+
7. (1/a) < e
⊢ ∃b:ℕ+. 1 + (1/b) < (1/q)
2
1. e : ℚ
2. q : ℚ
3. 0 < e
4. e ≤ q
5. q < 1
6. a : ℕ+
7. (1/a) < e
8. ∃b:ℕ+. 1 + (1/b) < (1/q)
⊢ ∃N:ℕ+. q ↑ N < e
Latex:
Latex:
1. e : \mBbbQ{}
2. q : \mBbbQ{}
3. 0 < e
4. e \mleq{} q
5. q < 1
6. a : \mBbbN{}\msupplus{}
7. (1/a) < e
\mvdash{} \mexists{}N:\mBbbN{}\msupplus{}. q \muparrow{} N < e
By
Latex:
Assert \mkleeneopen{}\mexists{}b:\mBbbN{}\msupplus{}. 1 + (1/b) < (1/q)\mkleeneclose{}\mcdot{}
Home
Index