Nuprl Lemma : logseq-converges-ext
∀a:{a:ℝ| r0 < a} . ∀b:{b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} . lim n→∞.logseq(a;b;n) = rlog(a)
Proof
Definitions occuring in Statement :
logseq: logseq(a;b;n),
rlog: rlog(x),
converges-to: lim n→∞.x[n] = y,
rdiv: (x/y),
rleq: x ≤ y,
rless: x < y,
rabs: |x|,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
member: t ∈ T,
logseq-converges
Lemmas referenced :
logseq-converges
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}a:\{a:\mBbbR{}| r0 < a\} . \mforall{}b:\{b:\mBbbR{}| |b - rlog(a)| \mleq{} (r1/r(10))\} . lim n\mrightarrow{}\minfty{}.logseq(a;b;n) = rlog(a)
Date html generated:
2016_10_26-PM-00_37_29
Last ObjectModification:
2016_09_18-PM-10_07_31
Theory : reals_2
Home
Index