### Nuprl Lemma : rinv-limit

`∀x:ℕ ⟶ ℝ. ∀a:ℝ.  (lim n→∞.x[n] = a `` (∀n:ℕ. x[n] ≠ r0) `` a ≠ r0 `` lim n→∞.(r1/x[n]) = (r1/a))`

Proof

Definitions occuring in Statement :  converges-to: `lim n→∞.x[n] = y` rdiv: `(x/y)` rneq: `x ≠ y` int-to-real: `r(n)` real: `ℝ` nat: `ℕ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` converges-to: `lim n→∞.x[n] = y` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` so_lambda: `λ2x.t[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)` uimplies: `b supposing a` req_int_terms: `t1 ≡ t2` false: `False` not: `¬A` top: `Top` rsub: `x - y` rge: `x ≥ y` guard: `{T}` rneq: `x ≠ y` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` nat_plus: `ℕ+` rless: `x < y` sq_exists: `∃x:A [B[x]]` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` rdiv: `(x/y)` sq-all-large: `∀large(n).{P[n]}` nat: `ℕ` rat_term_to_real: `rat_term_to_real(f;t)` rtermDivide: `num "/" denom` rat_term_ind: rat_term_ind rtermVar: `rtermVar(var)` rtermConstant: `"const"` pi1: `fst(t)` rtermMultiply: `left "*" right` pi2: `snd(t)` ge: `i ≥ j ` subtype_rel: `A ⊆r B` absval: `|i|` cand: `A c∧ B` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` sq_type: `SQType(T)`
Lemmas referenced :  rneq_wf int-to-real_wf istype-nat converges-to_wf real_wf radd-preserves-rleq rsub_wf rabs_wf radd_wf rminus_wf itermSubtract_wf itermAdd_wf itermVar_wf itermMinus_wf rleq_functionality radd_functionality req_weakening rabs_functionality req-iff-rsub-is-0 real_polynomial_null istype-int real_term_value_sub_lemma istype-void real_term_value_add_lemma real_term_value_var_lemma real_term_value_const_lemma real_term_value_minus_lemma rleq_weakening_equal rabs-difference-symmetry rleq_functionality_wrt_implies r-triangle-inequality rabs-neq-zero rmul_preserves_rless rdiv_wf rless-int rless_wf rless-int-fractions2 nat_plus_properties decidable__lt full-omega-unsat intformnot_wf intformless_wf itermConstant_wf int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_formula_prop_wf istype-less_than rmul_wf rinv_wf2 itermMultiply_wf rless_functionality req_transitivity rinv-mul-as-rdiv real_term_value_mul_lemma small-reciprocal-real istype-le assert-rat-term-eq2 rtermMultiply_wf rtermDivide_wf rtermConstant_wf rtermVar_wf rless_transitivity2 nat_properties intformand_wf int_formula_prop_and_lemma int_term_value_var_lemma radd-preserves-rless squash_wf true_wf radd_comm_eq subtype_rel_self iff_weakening_equal rmul-rinv3 radd_comm nat_plus_wf int_term_value_mul_lemma rneq_functionality rmul-int rneq-int intformeq_wf int_formula_prop_eq_lemma set_subtype_base less_than_wf int_subtype_base rmul_functionality req_inversion rinv_functionality2 rinv-of-rmul sq-all-large-and rleq_wf rpositive-rless rabs-positive absval_wf rabs-rmul rabs-rdiv rabs-int rmul_preserves_rleq rinv-as-rdiv rmul-rinv rleq_weakening_rless rabs-rmul-rleq square-nonzero req-int-fractions nequal_wf nat_plus_inc_int_nzero decidable__equal_int req_functionality rmul-rdiv-cancel5 int_entire_a subtype_base_sq rminus_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalHypSubstitution cut universeIsType introduction extract_by_obid isectElimination thin hypothesisEquality natural_numberEquality hypothesis sqequalRule functionIsType applyEquality lambdaEquality_alt because_Cache productElimination independent_isectElimination dependent_functionElimination approximateComputation int_eqEquality equalityTransitivity equalitySymmetry isect_memberEquality_alt voidElimination independent_functionElimination closedConclusion inrFormation_alt independent_pairFormation imageMemberEquality baseClosed dependent_set_memberEquality_alt setElimination rename unionElimination dependent_pairFormation_alt inhabitedIsType imageElimination instantiate universeEquality multiplyEquality equalityIstype baseApply intEquality sqequalBase cumulativity

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}a:\mBbbR{}.    (lim  n\mrightarrow{}\minfty{}.x[n]  =  a  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  x[n]  \mneq{}  r0)  {}\mRightarrow{}  a  \mneq{}  r0  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.(r1/x[n])  =  (r1/a))

Date html generated: 2019_10_29-AM-10_22_43
Last ObjectModification: 2019_04_02-PM-04_08_58

Theory : reals

Home Index