---

Step * 1 1 4 1 1 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. 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)
⊢ |rlog(e^(r(c1))/j) - rlog(a)| ≤ (r1/r(N))
BY
{ Assert ⌜r1 ≤ rmin(a;e^(r(c1))/j)⌝⋅ }

1
.....assertion..... 
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)
⊢ r1 ≤ rmin(a;e^(r(c1))/j)

2
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)
18. r1 ≤ rmin(a;e^(r(c1))/j)
⊢ |rlog(e^(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.  c1  :  \mBbbZ{}
13.  j  :  \mBbbN{}\msupplus{}
14.  |real\_exp((r(c1))/j)  -  a|  \mleq{}  (r1/r(N))
15.  (r0)/1  \mleq{}  (r(c1))/j
16.  (r(c1))/j  \mleq{}  (r(b))/1
17.  (r(c1))/j  =  rlog(e\^{}(r(c1))/j)
\mvdash{}  |rlog(e\^{}(r(c1))/j)  -  rlog(a)|  \mleq{}  (r1/r(N))


By

---

Latex:
Assert  \mkleeneopen{}r1  \mleq{}  rmin(a;e\^{}(r(c1))/j)\mkleeneclose{}\mcdot{}

---

Home Index