---

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


1. ∀a:{a:ℝ| r1 ≤ a} . ∀N:ℕ+.  ∃m:ℕ+. (∃z:ℤ [(|(r(z))/m - rlog(a)| ≤ (r1/r(N)))])
2. a : {a:ℝ| r0 < a} 
3. N : ℕ+
4. |r0 - rlog(a)| ≤ (|r1 - a|/rmin(a;r1))
5. r0 < rmin(a;r1)
6. a < r1
7. r1 ≤ (r1/a)
8. ∃m:ℕ+. (∃z:ℤ [(|(r(z))/m - rlog((r1/a))| ≤ (r1/r(N)))])
⊢ ∃m:ℕ+. (∃z:ℤ [(|(r(z))/m - rlog(a)| ≤ (r1/r(N)))])
BY
{ (ParallelLast THEN ExRepD THEN D 0 With ⌜-z⌝  THEN Auto) }

1
1. ∀a:{a:ℝ| r1 ≤ a} . ∀N:ℕ+.  ∃m:ℕ+. (∃z:ℤ [(|(r(z))/m - rlog(a)| ≤ (r1/r(N)))])
2. a : {a:ℝ| r0 < a} 
3. N : ℕ+
4. |r0 - rlog(a)| ≤ (|r1 - a|/rmin(a;r1))
5. r0 < rmin(a;r1)
6. a < r1
7. r1 ≤ (r1/a)
8. m : ℕ+
9. z : ℤ
10. |(r(z))/m - rlog((r1/a))| ≤ (r1/r(N))
⊢ |(r(-z))/m - rlog(a)| ≤ (r1/r(N))

---

Latex:

---

Latex:

1.  \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)))])
2.  a  :  \{a:\mBbbR{}|  r0  <  a\} 
3.  N  :  \mBbbN{}\msupplus{}
4.  |r0  -  rlog(a)|  \mleq{}  (|r1  -  a|/rmin(a;r1))
5.  r0  <  rmin(a;r1)
6.  a  <  r1
7.  r1  \mleq{}  (r1/a)
8.  \mexists{}m:\mBbbN{}\msupplus{}.  (\mexists{}z:\mBbbZ{}  [(|(r(z))/m  -  rlog((r1/a))|  \mleq{}  (r1/r(N)))])
\mvdash{}  \mexists{}m:\mBbbN{}\msupplus{}.  (\mexists{}z:\mBbbZ{}  [(|(r(z))/m  -  rlog(a)|  \mleq{}  (r1/r(N)))])


By

---

Latex:
(ParallelLast  THEN  ExRepD  THEN  D  0  With  \mkleeneopen{}-z\mkleeneclose{}    THEN  Auto)

---

Home Index