---

Step * 1 1 4 of Lemma near-log-exists


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...}
12. ∃c:ℤ. (∃j:ℕ+ [((|real_exp((r(c))/j) - a| ≤ (r1/r(N))) ∧ ((r0)/1 ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/1))])
⊢ ∃m:ℕ+. (∃z:ℤ [(|(r(z))/m - rlog(a)| ≤ (r1/r(N)))])
BY
{ (ExRepD
   THEN (InstConcl [⌜j⌝;⌜c1⌝]⋅ THENA Auto)
   THEN (Assert (r(c1))/j = rlog(e^(r(c1))/j) BY
               (RWO  "rlog-rexp" 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...}
12. c1 : ℤ
13. j : ℕ+
14. |real_exp((r(c1))/j) - a| ≤ (r1/r(N))
15. (r0)/1 ≤ (r(c1))/j
16. (r(c1))/j ≤ (r(b))/1
17. (r(c1))/j = rlog(e^(r(c1))/j)
⊢ |(r(c1))/j - rlog(a)| ≤ (r1/r(N))

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  r1  \mleq{}  a\} 
2.  N  :  \mBbbN{}\msupplus{}
3.  b  :  \mBbbN{}\msupplus{}
4.  a  \mleq{}  r(b)
5.  r1  \mleq{}  a
6.  r0  <  r1
7.  (r1  +  r(b))  \mleq{}  e\^{}r(b)
8.  c  :  \{2...\}
9.  e\^{}r(b)  \mleq{}  r(c)
10.  M  :  \{2...\}
11.  M  =  (N  *  c)
12.  \mexists{}c:\mBbbZ{}
          (\mexists{}j:\mBbbN{}\msupplus{}  [((|real\_exp((r(c))/j)  -  a|  \mleq{}  (r1/r(N)))
                        \mwedge{}  ((r0)/1  \mleq{}  (r(c))/j)
                        \mwedge{}  ((r(c))/j  \mleq{}  (r(b))/1))])
\mvdash{}  \mexists{}m:\mBbbN{}\msupplus{}.  (\mexists{}z:\mBbbZ{}  [(|(r(z))/m  -  rlog(a)|  \mleq{}  (r1/r(N)))])


By

---

Latex:
(ExRepD
  THEN  (InstConcl  [\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  (r(c1))/j  =  rlog(e\^{}(r(c1))/j)  BY
                          (RWO    "rlog-rexp"  0  THEN  Auto)))

---

Home Index