Step
*
1
1
2
of Lemma
qlog-bound
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
BY
{ xxx(Assert 1 < a BY
(SupposeNot
THEN (Assert a = 1 ∈ ℤ BY
Auto')
THEN Eliminate ⌜a⌝⋅
THEN Subst ⌜(1/1) = 1 ∈ ℚ⌝ (-4)⋅
THEN Auto
THEN Assert ⌜1 < 1⌝⋅
THEN Try ((RWO "qless-int" (-1) THEN Auto))
THEN RelRST
THEN Auto))xxx }
1
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)
9. 1 < a
⊢ ∃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
8. \mexists{}b:\mBbbN{}\msupplus{}. 1 + (1/b) < (1/q)
\mvdash{} \mexists{}N:\mBbbN{}\msupplus{}. q \muparrow{} N < e
By
Latex:
xxx(Assert 1 < a BY
(SupposeNot
THEN (Assert a = 1 BY
Auto')
THEN Eliminate \mkleeneopen{}a\mkleeneclose{}\mcdot{}
THEN Subst \mkleeneopen{}(1/1) = 1\mkleeneclose{} (-4)\mcdot{}
THEN Auto
THEN Assert \mkleeneopen{}1 < 1\mkleeneclose{}\mcdot{}
THEN Try ((RWO "qless-int" (-1) THEN Auto))
THEN RelRST
THEN Auto))xxx
Home
Index