---

Step * 1 of Lemma qlog-bound


1. e : {e:ℚ| 0 < e} 
2. q : {q:ℚ| (e ≤ q) ∧ q < 1} 
⊢ ∃N:ℕ+. q ↑ N < e
BY
{ xxx((Decide 0 < e THENA Auto)
      THEN Try (Complete ((D (-1) THEN D 1 THEN Unhide THEN Auto)))
      THEN D 1
      THEN Thin 2
      THEN (Decide ⌜(e ≤ q) ∧ q < 1⌝⋅ THENA Auto)
      THEN Try (Complete ((D (-1) THEN D 2 THEN Unhide THEN Auto)))
      THEN D 2
      THEN Thin 3
      THEN (InstLemma `small-reciprocal` [⌜e⌝]⋅ THENA Auto)
      THEN ExRepD
      THEN RenameVar `a' (-2))xxx }

1
1. e : ℚ
2. q : ℚ
3. 0 < e
4. e ≤ q
5. q < 1
6. a : ℕ+
7. (1/a) < e
⊢ ∃N:ℕ+. q ↑ N < e

---

Latex:

---

Latex:

1.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
2.  q  :  \{q:\mBbbQ{}|  (e  \mleq{}  q)  \mwedge{}  q  <  1\} 
\mvdash{}  \mexists{}N:\mBbbN{}\msupplus{}.  q  \muparrow{}  N  <  e


By

---

Latex:
xxx((Decide  0  <  e  THENA  Auto)
        THEN  Try  (Complete  ((D  (-1)  THEN  D  1  THEN  Unhide  THEN  Auto)))
        THEN  D  1
        THEN  Thin  2
        THEN  (Decide  \mkleeneopen{}(e  \mleq{}  q)  \mwedge{}  q  <  1\mkleeneclose{}\mcdot{}  THENA  Auto)
        THEN  Try  (Complete  ((D  (-1)  THEN  D  2  THEN  Unhide  THEN  Auto)))
        THEN  D  2
        THEN  Thin  3
        THEN  (InstLemma  `small-reciprocal`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  ExRepD
        THEN  RenameVar  `a'  (-2))xxx

---

Home Index