Nuprl Lemma : rinv-converges-to-0

lim n→∞.(r1/r(n 1)) r0


Proof




Definitions occuring in Statement :  converges-to: lim n→∞.x[n] y rdiv: (x/y) int-to-real: r(n) add: m natural_number: $n
Definitions unfolded in proof :  converges-to: lim n→∞.x[n] y all: x:A. B[x] member: t ∈ T sq_exists: x:{A| B[x]} subtype_rel: A ⊆B implies:  Q prop: uall: [x:A]. B[x] nat_plus: + nat: so_lambda: λ2x.t[x] uimplies: supposing a rneq: x ≠ y guard: {T} or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q ge: i ≥  decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top so_apply: x[s] rdiv: (x/y) itermConstant: "const" req_int_terms: t1 ≡ t2 uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) le: A ≤ B subtract: m less_than': less_than'(a;b) true: True
Lemmas referenced :  nat_plus_wf nat_plus_subtype_nat le_wf nat_wf all_wf rleq_wf rabs_wf rsub_wf rdiv_wf int-to-real_wf rless-int nat_properties nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermAdd_wf itermVar_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf rless_wf rmul_wf rinv_wf2 uiff_transitivity rleq_functionality rabs_functionality real_term_polynomial itermSubtract_wf itermMultiply_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma req-iff-rsub-is-0 rinv-as-rdiv rleq-int-fractions2 false_wf not-lt-2 less-iff-le condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero add-swap le-add-cancel less_than_wf decidable__le int_term_value_mul_lemma rleq-int-fractions rabs-of-nonneg req_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid hypothesis dependent_set_memberFormation hypothesisEquality applyEquality sqequalHypSubstitution sqequalRule isectElimination thin setElimination rename lambdaEquality functionEquality because_Cache natural_numberEquality addEquality independent_isectElimination inrFormation dependent_functionElimination productElimination independent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll dependent_set_memberEquality minusEquality multiplyEquality

Latex:
lim  n\mrightarrow{}\minfty{}.(r1/r(n  +  1))  =  r0



Date html generated: 2017_10_03-AM-08_51_45
Last ObjectModification: 2017_07_28-AM-07_34_49

Theory : reals


Home Index