---

Step * of Lemma logseq-property

∀a:{a:ℝ| r0 < a} . ∀b:{b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} . ∀n:ℕ.  (|logseq(a;b;n) - rlog(a)| ≤ (r1/r(10^3^n)))
BY
{ InductionOnNat }

1
.....basecase..... 
1. a : {a:ℝ| r0 < a} 
2. b : {b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} 
3. n : ℤ
⊢ |logseq(a;b;0) - rlog(a)| ≤ (r1/r(10^3^0))

2
.....upcase..... 
1. a : {a:ℝ| r0 < a} 
2. b : {b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} 
3. n : ℤ
4. 0 < n
5. |logseq(a;b;n - 1) - rlog(a)| ≤ (r1/r(10^3^(n - 1)))
⊢ |logseq(a;b;n) - rlog(a)| ≤ (r1/r(10^3^n))

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  r0  <  a\}  .  \mforall{}b:\{b:\mBbbR{}|  |b  -  rlog(a)|  \mleq{}  (r1/r(10))\}  .  \mforall{}n:\mBbbN{}.
    (|logseq(a;b;n)  -  rlog(a)|  \mleq{}  (r1/r(10\^{}3\^{}n)))


By

---

Latex:
InductionOnNat

---

Home Index