Nuprl Lemma : alternating-series-converges-ext
∀x:ℕ ⟶ ℝ. ((∃M:ℕ. ∀n:ℕ. (M < n ⇒ ((r0 ≤ x[n]) ∧ (x[n + 1] ≤ x[n])))) ⇒ lim n→∞.x[n] = r0 ⇒ Σn.-1^n * x[n]↓)
Proof
Definitions occuring in Statement :
series-converges: Σn.x[n]↓,
converges-to: lim n→∞.x[n] = y,
rleq: x ≤ y,
int-rmul: k1 * a,
int-to-real: r(n),
real: ℝ,
fastexp: i^n,
nat: ℕ,
less_than: a < b,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
add: n + m,
minus: -n,
natural_number: $n
Definitions unfolded in proof :
member: t ∈ T,
so_apply: x[s],
int-rmul: k1 * a,
so_lambda: λ2x.t[x],
accelerate: accelerate(k;f),
alternating-series-converges,
converges-iff-cauchy-ext
Lemmas referenced :
alternating-series-converges,
converges-iff-cauchy-ext
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}x:\mBbbN{} {}\mrightarrow{} \mBbbR{}
((\mexists{}M:\mBbbN{}. \mforall{}n:\mBbbN{}. (M < n {}\mRightarrow{} ((r0 \mleq{} x[n]) \mwedge{} (x[n + 1] \mleq{} x[n]))))
{}\mRightarrow{} lim n\mrightarrow{}\minfty{}.x[n] = r0
{}\mRightarrow{} \mSigma{}n.-1\^{}n * x[n]\mdownarrow{})
Date html generated:
2019_10_29-AM-10_29_52
Last ObjectModification:
2019_04_02-AM-10_56_57
Theory : reals
Home
Index