Nuprl Lemma : rinv-exp-converges-ext
∀M:ℕ+. ∀N:{2...}. lim n→∞.(r1/r(M * N^n)) = r0
Proof
Definitions occuring in Statement :
converges-to: lim n→∞.x[n] = y,
rdiv: (x/y),
int-to-real: r(n),
exp: i^n,
int_upper: {i...},
nat_plus: ℕ+,
all: ∀x:A. B[x],
multiply: n * m,
natural_number: $n
Definitions unfolded in proof :
member: t ∈ T,
rinv-exp-converges
Lemmas referenced :
rinv-exp-converges
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}M:\mBbbN{}\msupplus{}. \mforall{}N:\{2...\}. lim n\mrightarrow{}\minfty{}.(r1/r(M * N\^{}n)) = r0
Date html generated:
2016_10_26-AM-09_16_36
Last ObjectModification:
2016_09_04-PM-02_07_00
Theory : reals
Home
Index