Nuprl Lemma : expfact-property

k:ℕ. ∀n:ℕ+.  ∃m:ℕ+((n k^m) ≤ (m)!)


Proof




Definitions occuring in Statement :  fact: (n)! exp: i^n nat_plus: + nat: le: A ≤ B all: x:A. B[x] exists: x:A. B[x] multiply: m
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T subtype_rel: A ⊆B exists: x:A. B[x] uall: [x:A]. B[x] nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True and: P ∧ Q prop: nat: implies:  Q decidable: Dec(P) or: P ∨ Q uimplies: supposing a sq_type: SQType(T) guard: {T} ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top iff: ⇐⇒ Q rev_implies:  Q so_lambda: λ2x.t[x] so_apply: x[s] fact: (n)! primrec: primrec(n;b;c) subtract: m le: A ≤ B sq_stable: SqStable(P) uiff: uiff(P;Q)
Lemmas referenced :  equal_wf multiply-is-int-iff sq_stable__le set_wf nat_plus_subtype_nat le_wf false_wf set_subtype_base iff_weakening_equal exp1 int_term_value_mul_lemma int_formula_prop_less_lemma itermMultiply_wf intformless_wf fact0_redex_lemma exp0_lemma int_formula_prop_wf int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformeq_wf itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_plus_properties nat_properties int_subtype_base subtype_base_sq decidable__equal_int fact_wf exp_wf2 less_than_wf expfact_wf nat_wf nat_plus_wf fact-greater-exp
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality applyEquality because_Cache hypothesis sqequalRule productElimination isectElimination dependent_set_memberEquality natural_numberEquality independent_pairFormation introduction imageMemberEquality baseClosed multiplyEquality setElimination rename lambdaEquality independent_functionElimination unionElimination instantiate cumulativity intEquality independent_isectElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality computeAll equalityEquality equalityTransitivity equalitySymmetry setEquality imageElimination pointwiseFunctionality promote_hyp baseApply closedConclusion

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}n:\mBbbN{}\msupplus{}.    \mexists{}m:\mBbbN{}\msupplus{}.  ((n  *  k\^{}m)  \mleq{}  (m)!)



Date html generated: 2016_05_15-PM-04_07_08
Last ObjectModification: 2016_01_16-AM-11_02_43

Theory : general


Home Index