Nuprl Lemma : rdiv-factorial-limit-zero-from-bound

x:ℝ. ∀n:ℕ.  ((|x| ≤ r(n))  lim n→∞.(|x|^n/r((n)!)) r0)


Proof




Definitions occuring in Statement :  converges-to: lim n→∞.x[n] y rdiv: (x/y) rleq: x ≤ y rabs: |x| rnexp: x^k1 int-to-real: r(n) real: nat: all: x:A. B[x] implies:  Q natural_number: $n fact: (n)!
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q converges-to: lim n→∞.x[n] y member: t ∈ T exists: x:A. B[x] prop: uall: [x:A]. B[x] nat: sq_exists: x:{A| B[x]} subtype_rel: A ⊆B nat_plus: + 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) not: ¬A false: False satisfiable_int_formula: satisfiable_int_formula(fmla) 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) real: le: A ≤ B rnonneg: rnonneg(x) rleq: x ≤ y rge: x ≥ y sq_type: SQType(T) squash: T less_than: a < b subtract: m assert: b bnot: ¬bb bfalse: ff ifthenelse: if then else fi  btrue: tt it: unit: Unit bool: 𝔹 nequal: a ≠ b ∈ 
Lemmas referenced :  expfact-property nat_plus_wf rleq_wf rabs_wf int-to-real_wf nat_wf real_wf nat_plus_subtype_nat le_wf all_wf rsub_wf rdiv_wf rnexp_wf fact_wf rless-int nat_properties nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformless_wf itermConstant_wf itermVar_wf intformnot_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_formula_prop_wf rless_wf rmul_wf rinv_wf2 rleq_functionality rabs_functionality req_transitivity 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-mul-as-rdiv rinv-as-rdiv rabs-of-nonneg rmul-rdiv-cancel2 req_weakening rmul-int uiff_transitivity less_than_wf exp_wf_nat_plus decidable__le rmul_preserves_rleq zero-rleq-rabs rnexp-nonneg zero-mul rnexp-rleq rmul-int-rdiv rmul_comm rnexp-int exp_wf2 less_than'_wf int_formula_prop_le_lemma intformle_wf rleq-int rmul_preserves_rleq2 rleq_weakening_equal rleq_functionality_wrt_implies int_subtype_base subtype_base_sq decidable__equal_int int_formula_prop_eq_lemma intformeq_wf exp_preserves_lt false_wf int_term_value_mul_lemma multiply-is-int-iff exp_wf4 mul_preserves_le fact-bound int_term_value_subtract_lemma subtract_wf int_term_value_add_lemma itermAdd_wf add-zero ge_wf exp_step add-associates add-commutes add-swap mul-swap le_weakening le_functionality neg_assert_of_eq_int assert-bnot bool_subtype_base bool_cases_sqequal equal_wf eqff_to_assert assert_of_eq_int eqtt_to_assert bool_wf eq_int_wf fact_unroll trivial-int-eq1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality productElimination hypothesis isectElimination setElimination rename dependent_set_memberFormation applyEquality sqequalRule lambdaEquality functionEquality because_Cache independent_isectElimination inrFormation independent_functionElimination natural_numberEquality dependent_set_memberEquality unionElimination equalityTransitivity equalitySymmetry applyLambdaEquality voidElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidEquality independent_pairFormation computeAll multiplyEquality axiomEquality minusEquality independent_pairEquality isect_memberFormation cumulativity instantiate imageElimination baseClosed closedConclusion baseApply promote_hyp pointwiseFunctionality addEquality intWeakElimination equalityElimination

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}.    ((|x|  \mleq{}  r(n))  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.(|x|\^{}n/r((n)!))  =  r0)



Date html generated: 2017_10_03-AM-09_26_44
Last ObjectModification: 2017_07_28-AM-07_46_55

Theory : reals


Home Index