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: P ⇒ Q, natural_number: $n, fact: (n)!
Definitions unfolded in proof : all: ∀x:A. B[x], implies: P ⇒ 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 ⊆r B, nat_plus: ℕ⁺, so_lambda: λ₂x.t[x], uimplies: b supposing a, rneq: x ≠ y, guard: {T}, or: P ∨ Q, iff: P ⇐⇒ Q, and: P ∧ Q, rev_implies: P ⇐ Q, ge: i ≥ j , 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: n - m, assert: ↑b, bnot: ¬_bb, bfalse: ff, ifthenelse: if b then t else f fi , btrue: tt, it: ⋅, unit: Unit, bool: 𝔹, nequal: a ≠ b ∈ T
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