---

Step * 1 of Lemma near-log-exists

.....assertion..... 
∀a:{a:ℝ| r1 ≤ a} . ∀N:ℕ+.  ∃m:ℕ+. (∃z:ℤ [(|(r(z))/m - rlog(a)| ≤ (r1/r(N)))])
BY
{ (Auto
   THEN (InstLemma `r-archimedean` [⌜a⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (Evaluate ⌜b = n ∈ ℕ+⌝⋅
         THENA (Auto THEN (Assert (r1 ≤ a) ∧ (r1 ≤ r(n)) BY Auto) THEN RWO "rleq-int" (-1) THEN Auto)
         )
   THEN (Assert a ≤ r(b) BY
               Auto)
   THEN ThinVar `n'
   THEN (Assert r1 ≤ a BY
               Auto)
   THEN (Assert r0 < r1 BY
               Auto)
   THEN (InstLemma `rexp-of-nonneg-stronger` [⌜r(b)⌝]⋅ THENA Auto)
   THEN (InstLemma `r-archimedean` [⌜real_exp(r(b))⌝]⋅ THENA Auto)
   THEN (RWO "real_exp-req" (-1) THENA Auto)
   THEN ExRepD
   THEN (Evaluate ⌜c = n ∈ {2...}⌝⋅
         THENA (Auto
                THEN (Assert (r1 + r(b)) ≤ r(n) BY
                            Auto)
                THEN (RWO  "radd-int" (-1) THENA Auto)
                THEN RWO "rleq-int" (-1)
                THEN Auto)
         )
   THEN (Assert e^r(b) ≤ r(c) BY
               Auto)
   THEN ThinVar `n'
   THEN (Evaluate ⌜M = (N * c) ∈ {2...}⌝⋅
         THENA (Auto
                THEN (Assert 2 ≤ c BY
                            Auto)
                THEN (Assert 1 ≤ N BY
                            Auto)
                THEN MemTypeCD
                THEN Auto
                THEN RWO  "-2<" 0
                THEN Auto)
         )) }

1
1. a : {a:ℝ| r1 ≤ a} 
2. N : ℕ+
3. b : ℕ+
4. a ≤ r(b)
5. r1 ≤ a
6. r0 < r1
7. (r1 + r(b)) ≤ e^r(b)
8. c : {2...}
9. e^r(b) ≤ r(c)
10. M : {2...}
11. M = (N * c) ∈ {2...}
⊢ ∃m:ℕ+. (∃z:ℤ [(|(r(z))/m - rlog(a)| ≤ (r1/r(N)))])

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}a:\{a:\mBbbR{}|  r1  \mleq{}  a\}  .  \mforall{}N:\mBbbN{}\msupplus{}.    \mexists{}m:\mBbbN{}\msupplus{}.  (\mexists{}z:\mBbbZ{}  [(|(r(z))/m  -  rlog(a)|  \mleq{}  (r1/r(N)))])


By

---

Latex:
(Auto
  THEN  (InstLemma  `r-archimedean`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Evaluate  \mkleeneopen{}b  =  n\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  (Assert  (r1  \mleq{}  a)  \mwedge{}  (r1  \mleq{}  r(n))  BY  Auto)  THEN  RWO  "rleq-int"  (-1)  THEN  Auto)
              )
  THEN  (Assert  a  \mleq{}  r(b)  BY
                          Auto)
  THEN  ThinVar  `n'
  THEN  (Assert  r1  \mleq{}  a  BY
                          Auto)
  THEN  (Assert  r0  <  r1  BY
                          Auto)
  THEN  (InstLemma  `rexp-of-nonneg-stronger`  [\mkleeneopen{}r(b)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `r-archimedean`  [\mkleeneopen{}real\_exp(r(b))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "real\_exp-req"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (Evaluate  \mkleeneopen{}c  =  n\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  (Assert  (r1  +  r(b))  \mleq{}  r(n)  BY
                                                    Auto)
                            THEN  (RWO    "radd-int"  (-1)  THENA  Auto)
                            THEN  RWO  "rleq-int"  (-1)
                            THEN  Auto)
              )
  THEN  (Assert  e\^{}r(b)  \mleq{}  r(c)  BY
                          Auto)
  THEN  ThinVar  `n'
  THEN  (Evaluate  \mkleeneopen{}M  =  (N  *  c)\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  (Assert  2  \mleq{}  c  BY
                                                    Auto)
                            THEN  (Assert  1  \mleq{}  N  BY
                                                    Auto)
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  RWO    "-2<"  0
                            THEN  Auto)
              ))

---

Home Index