### Nuprl Lemma : rpowers-converge-ext

`∀x:ℝ. (((|x| < r1) `` lim n→∞.x^n = r0) ∧ ((r1 < x) `` lim n →∞.x^n = ∞))`

Proof

Definitions occuring in Statement :  converges-to-infinity: `lim n →∞.x[n] = ∞` converges-to: `lim n→∞.x[n] = y` rless: `x < y` rabs: `|x|` rnexp: `x^k1` int-to-real: `r(n)` real: `ℝ` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` natural_number: `\$n`
Definitions unfolded in proof :  member: `t ∈ T` rabs: `|x|` int-to-real: `r(n)` rsub: `x - y` rminus: `-(x)` canonical-bound: `canonical-bound(r)` rpowers-converge rnexp-converges integer-bound rless_transitivity2 rless-int rleq_weakening_rless rationals-dense-ext uall: `∀[x:A]. B[x]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  rpowers-converge lifting-strict-callbyvalue istype-void strict4-spread rnexp-converges integer-bound rless_transitivity2 rless-int rleq_weakening_rless rationals-dense-ext
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed isect_memberEquality_alt voidElimination independent_isectElimination

Latex:
\mforall{}x:\mBbbR{}.  (((|x|  <  r1)  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x\^{}n  =  r0)  \mwedge{}  ((r1  <  x)  {}\mRightarrow{}  lim  n  \mrightarrow{}\minfty{}.x\^{}n  =  \minfty{}))

Date html generated: 2019_10_29-AM-10_10_35
Last ObjectModification: 2019_04_01-PM-10_59_29

Theory : reals

Home Index