Nuprl Lemma : exp-ratio-property2
∀M:ℕ+. ∀b:{2...}. ∀k:ℕ. (exp-ratio(1;b;0;k;M) ∈ {n:ℕ| k < M * b^n} )
Proof
Definitions occuring in Statement :
exp-ratio: exp-ratio(a;b;n;p;q),
exp: i^n,
int_upper: {i...},
nat_plus: ℕ+,
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
member: t ∈ T,
set: {x:A| B[x]} ,
multiply: n * m,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
exp-ratio_wf2,
nat_wf,
int_upper_wf,
nat_plus_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
hypothesis,
isectElimination,
natural_numberEquality
Latex:
\mforall{}M:\mBbbN{}\msupplus{}. \mforall{}b:\{2...\}. \mforall{}k:\mBbbN{}. (exp-ratio(1;b;0;k;M) \mmember{} \{n:\mBbbN{}| k < M * b\^{}n\} )
Date html generated:
2016_10_25-AM-10_52_01
Last ObjectModification:
2016_09_04-PM-05_55_32
Theory : general
Home
Index