Nuprl Lemma : increasing-sequence-converges

∀x:ℕ ⟶ ℝ
  ((∀n:ℕ. ((x n) < (x (n + 1))))
  ⇒ (∃c:{2...}
       ∃m:ℕ+
        ((∀n:ℕ+. (((x (n + 1)) - x n) ≤ ((r1/r(c)) * ((x n) - x (n - 1)))))
        ∧ ((r(c) * ((x 1) - x 0)/r(c - 1)) ≤ (r1/r(m)))))
  ⇒ x n↓ as n→∞)


Proof



Definitions occuring in Statement :  converges: x[n]↓ as n→∞,  rdiv: (x/y),  rleq: x ≤ y,  rless: x < y,  rsub: x - y,  rmul: a * b,  int-to-real: r(n),  real: ℝ,  int_upper: {i...},  nat_plus: ℕ+,  nat: ℕ,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  apply: f a,  function: x:A ⟶ B[x],  subtract: n - m,  add: n + m,  natural_number: $n
Definitions unfolded in proof :  all: ∀x:A. B[x],  implies: P ⇒ Q,  exists: ∃x:A. B[x],  and: P ∧ Q,  member: t ∈ T,  prop: ℙ,  uall: ∀[x:A]. B[x],  so_lambda: λ2x.t[x],  nat: ℕ,  nat_plus: ℕ+,  guard: {T},  int_upper: {i...},  decidable: Dec(P),  or: P ∨ Q,  uimplies: b supposing a,  satisfiable_int_formula: satisfiable_int_formula(fmla),  false: False,  not: ¬A,  top: Top,  subtype_rel: A ⊆r B,  rneq: x ≠ y,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  so_apply: x[s],  le: A ≤ B,  less_than': less_than'(a;b),  ge: i ≥ j ,  true: True,  uiff: uiff(P;Q),  subtract: n - m,  squash: ↓T,  less_than: a < b,  rge: x ≥ y,  rev_uimplies: rev_uimplies(P;Q),  rnonneg: rnonneg(x),  rleq: x ≤ y,  sq_type: SQType(T),  itermConstant: "const",  req_int_terms: t1 ≡ t2,  rless: x < y,  sq_exists: ∃x:{A| B[x]},  real: ℝ,  sq_stable: SqStable(P),  nequal: a ≠ b ∈ T ,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  bfalse: ff,  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  assert: ↑b,  rdiv: (x/y),  absval: |i|,  cand: A c∧ B,  cauchy: cauchy(n.x[n]),  converges-to: lim n→∞.x[n] = y,  rsub: x - y
Lemmas referenced :  exists_wf,  int_upper_wf,  nat_plus_wf,  all_wf,  rleq_wf,  rsub_wf,  nat_wf,  nat_plus_properties,  int_upper_properties,  decidable__le,  satisfiable-full-omega-tt,  intformand_wf,  intformnot_wf,  intformle_wf,  itermConstant_wf,  itermAdd_wf,  itermVar_wf,  intformless_wf,  int_formula_prop_and_lemma,  int_formula_prop_not_lemma,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  int_term_value_add_lemma,  int_term_value_var_lemma,  int_formula_prop_less_lemma,  int_formula_prop_wf,  le_wf,  nat_plus_subtype_nat,  rmul_wf,  rdiv_wf,  int-to-real_wf,  rless-int,  decidable__lt,  rless_wf,  subtract_wf,  itermSubtract_wf,  int_term_value_subtract_lemma,  false_wf,  nat_properties,  real_wf,  primrec-wf-nat-plus,  le-add-cancel,  zero-add,  add-commutes,  add_functionality_wrt_le,  not-lt-2,  less_than_wf,  exp-positive,  exp_wf2,  iff_weakening_equal,  exp1,  rneq_wf,  true_wf,  squash_wf,  rleq_weakening_equal,  rleq_functionality_wrt_implies,  add-subtract-cancel,  add-zero,  add-associates,  minus-one-mul-top,  minus-one-mul,  minus-add,  condition-implies-le,  less-iff-le,  equal_wf,  rmul_functionality,  rmul_comm,  rmul-assoc,  req_inversion,  req_weakening,  rleq_functionality,  uiff_transitivity,  less_than'_wf,  int_term_value_mul_lemma,  itermMultiply_wf,  rleq-int-fractions2,  rmul_preserves_rleq2,  exp_step,  int_subtype_base,  set_subtype_base,  subtype_base_sq,  exp_wf_nat_plus,  rmul-int-fractions,  req_functionality,  decidable__equal_int,  mul_nat_plus,  req-int-fractions,  int_formula_prop_eq_lemma,  intformeq_wf,  mul_bounds_1b,  radd-preserves-rless,  radd_wf,  rless_functionality,  real_term_polynomial,  real_term_value_const_lemma,  real_term_value_sub_lemma,  real_term_value_add_lemma,  real_term_value_var_lemma,  req-iff-rsub-is-0,  ge_wf,  rabs_wf,  less_than_transitivity1,  less_than_irreflexivity,  absval_wf,  imin_wf,  imin_nat,  sq_stable__less_than,  rneq-int,  int_entire_a,  equal-wf-base,  equal-wf-T-base,  absval-non-neg,  le-iff-imin,  absval_unfold,  lt_int_wf,  bool_wf,  eqtt_to_assert,  assert_of_lt_int,  top_wf,  eqff_to_assert,  bool_cases_sqequal,  bool_subtype_base,  assert-bnot,  itermMinus_wf,  int_term_value_minus_lemma,  radd-preserves-rleq,  rleq_weakening_rless,  rabs-of-nonneg,  r-triangle-inequality2,  minus-minus,  radd_functionality_wrt_rleq,  rabs-difference-symmetry,  radd-int-fractions,  rleq-int-fractions,  multiply-is-int-iff,  multiply_nat_plus,  rinv_wf2,  real_term_value_mul_lemma,  radd_functionality,  rinv-mul-as-rdiv,  rmul_preserves_req,  req_transitivity,  rmul-rinv3,  imin_unfold,  le_int_wf,  assert_of_le_int,  absval-diff-symmetry,  rabs_functionality,  uiff_transitivity2,  rabs-int,  minus-zero,  rmul_preserves_rleq,  rmul-nonneg-case1,  rleq-int,  add_nat_wf,  add-is-int-iff,  rmul-is-positive,  rdiv_functionality,  rmul-int,  rinv-of-rmul,  rmul-rinv,  rinv-as-rdiv,  rinv-exp-converges,  converges-iff-cauchy,  add-swap,  imin_ub,  radd-zero-both,  radd_comm,  rminus-zero,  rabs-bounds,  rminus_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation,  sqequalHypSubstitution,  productElimination,  thin,  cut,  introduction,  extract_by_obid,  isectElimination,  natural_numberEquality,  hypothesis,  sqequalRule,  lambdaEquality,  productEquality,  because_Cache,  applyEquality,  functionExtensionality,  hypothesisEquality,  dependent_set_memberEquality,  addEquality,  setElimination,  rename,  dependent_functionElimination,  unionElimination,  independent_isectElimination,  dependent_pairFormation,  int_eqEquality,  intEquality,  isect_memberEquality,  voidElimination,  voidEquality,  independent_pairFormation,  computeAll,  inrFormation,  independent_functionElimination,  functionEquality,  universeEquality,  equalitySymmetry,  equalityTransitivity,  imageElimination,  baseClosed,  imageMemberEquality,  minusEquality,  axiomEquality,  independent_pairEquality,  multiplyEquality,  isect_memberFormation,  cumulativity,  instantiate,  applyLambdaEquality,  intWeakElimination,  inlFormation,  baseApply,  closedConclusion,  equalityElimination,  lessCases,  sqequalAxiom,  promote_hyp,  pointwiseFunctionality,  sqequalIntensionalEquality,  addLevel,  impliesFunctionality,  dependent_set_memberFormation
Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}
    ((\mforall{}n:\mBbbN{}.  ((x  n)  <  (x  (n  +  1))))
    {}\mRightarrow{}  (\mexists{}c:\{2...\}
              \mexists{}m:\mBbbN{}\msupplus{}
                ((\mforall{}n:\mBbbN{}\msupplus{}.  (((x  (n  +  1))  -  x  n)  \mleq{}  ((r1/r(c))  *  ((x  n)  -  x  (n  -  1)))))
                \mwedge{}  ((r(c)  *  ((x  1)  -  x  0)/r(c  -  1))  \mleq{}  (r1/r(m)))))
    {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})


Date html generated: 2017_10_04-PM-10_23_49
Last ObjectModification: 2017_07_28-AM-08_48_41

Theory : reals_2


Home Index