---

Step * 2 of Lemma logseq-converges


1. a : {a:ℝ| r0 < a} 
2. b : {b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} 
3. k : ℕ+
4. ∃n:ℕ. (k ≤ 10^3^n)
⊢ ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|logseq(a;b;n) - rlog(a)| ≤ (r1/r(k)))))}
BY
{ ((ExRepD THEN D 0 With ⌜n⌝  THEN Auto) THEN RenameVar `m' (-2) THEN RWO "logseq-property" 0 THEN Auto) }

1
1. a : {a:ℝ| r0 < a} 
2. b : {b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} 
3. k : ℕ+
4. n : ℕ
5. k ≤ 10^3^n
6. m : ℕ
7. n ≤ m
⊢ (r1/r(10^3^m)) ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  r0  <  a\} 
2.  b  :  \{b:\mBbbR{}|  |b  -  rlog(a)|  \mleq{}  (r1/r(10))\} 
3.  k  :  \mBbbN{}\msupplus{}
4.  \mexists{}n:\mBbbN{}.  (k  \mleq{}  10\^{}3\^{}n)
\mvdash{}  \mexists{}N:\{\mBbbN{}|  (\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|logseq(a;b;n)  -  rlog(a)|  \mleq{}  (r1/r(k)))))\}


By

---

Latex:
((ExRepD  THEN  D  0  With  \mkleeneopen{}n\mkleeneclose{}    THEN  Auto)
  THEN  RenameVar  `m'  (-2)
  THEN  RWO  "logseq-property"  0
  THEN  Auto)

---

Home Index