### Nuprl Lemma : rmul-limit

`∀x,y:ℕ ⟶ ℝ. ∀a,b:ℝ.  (lim n→∞.x[n] = a `` lim n→∞.y[n] = b `` lim n→∞.x[n] * y[n] = a * b)`

Proof

Definitions occuring in Statement :  converges-to: `lim n→∞.x[n] = y` rmul: `a * b` real: `ℝ` nat: `ℕ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` converges-to: `lim n→∞.x[n] = y` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` converges: `x[n]↓ as n→∞` bounded-sequence: `bounded-sequence(n.x[n])` nat_plus: `ℕ+` guard: `{T}` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` top: `Top` and: `P ∧ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` nat: `ℕ` ge: `i ≥ j ` le: `A ≤ B` less_than': `less_than'(a;b)` subtype_rel: `A ⊆r B` less_than: `a < b` squash: `↓T` true: `True` sq-all-large: `∀large(n).{P[n]}` rneq: `x ≠ y` sq_exists: `∃x:{A| B[x]}` rsub: `x - y` uiff: `uiff(P;Q)` sq_stable: `SqStable(P)` rleq: `x ≤ y` rnonneg: `rnonneg(x)`
Lemmas referenced :  converges-to_wf nat_wf real_wf integer-bound converges-implies-bounded imax_wf imax_nat_plus nat_plus_wf nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_wf equal_wf less_than_wf rleq_wf rabs_wf int-to-real_wf all_wf rleq-int imax_ub decidable__le intformle_wf int_formula_prop_le_lemma le_wf rleq_functionality_wrt_implies rleq_weakening_equal rabs-bounds nat_properties mul_bounds_1a false_wf multiply_nat_wf nat_plus_subtype_nat mul_nat_plus sq-all-large-and rsub_wf rdiv_wf rless-int mul_bounds_1b rless_wf rmul_wf radd_wf r-triangle-inequality rminus_wf uiff_transitivity rleq_functionality req_weakening rabs_functionality radd_functionality req_transitivity rmul-distrib rmul_over_rminus req_inversion radd-assoc radd-ac radd-rminus-assoc rabs-rmul-rleq itermMultiply_wf int_term_value_mul_lemma rleq-int-fractions sq_stable__all sq_stable__rleq less_than'_wf squash_wf rmul-int-rdiv2 rmul-int-rdiv itermAdd_wf int_term_value_add_lemma uimplies_transitivity rdiv_functionality radd-int radd-rdiv radd_functionality_wrt_rleq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution cut introduction extract_by_obid isectElimination thin sqequalRule lambdaEquality applyEquality functionExtensionality hypothesisEquality hypothesis functionEquality dependent_functionElimination productElimination dependent_pairFormation independent_functionElimination dependent_set_memberEquality natural_numberEquality setElimination rename equalityTransitivity equalitySymmetry applyLambdaEquality unionElimination independent_isectElimination int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll productEquality because_Cache inrFormation inlFormation multiplyEquality imageMemberEquality baseClosed independent_pairEquality minusEquality axiomEquality imageElimination addEquality

Latex:
\mforall{}x,y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}a,b:\mBbbR{}.    (lim  n\mrightarrow{}\minfty{}.x[n]  =  a  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.y[n]  =  b  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  *  y[n]  =  a  *  b)

Date html generated: 2017_10_03-AM-09_05_48
Last ObjectModification: 2017_07_28-AM-07_41_44

Theory : reals

Home Index