---

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