### Nuprl Lemma : series-converges-rmul

c:ℝ. ∀x:ℕ ⟶ ℝ.  n.x[n]↓  Σn.x[n] c↓)

Proof

Definitions occuring in Statement :  series-converges: Σn.x[n]↓ rmul: b real: nat: so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q series-converges: Σn.x[n]↓ exists: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] prop:
Lemmas referenced :  rmul_wf series-sum-linear3 nat_wf series-sum_wf series-converges_wf real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin dependent_pairFormation cut lemma_by_obid isectElimination hypothesisEquality hypothesis dependent_functionElimination sqequalRule lambdaEquality applyEquality independent_functionElimination functionEquality

Latex:
\mforall{}c:\mBbbR{}.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.    (\mSigma{}n.x[n]\mdownarrow{}  {}\mRightarrow{}  \mSigma{}n.x[n]  *  c\mdownarrow{})

Date html generated: 2016_05_18-AM-07_58_49
Last ObjectModification: 2015_12_28-AM-01_09_15

Theory : reals

Home Index