Nuprl Lemma : fact-bound

n:ℕ((n)! ≤ n^n)


Proof




Definitions occuring in Statement :  fact: (n)! exp: i^n nat: le: A ≤ B all: x:A. B[x]
Definitions unfolded in proof :  or: P ∨ Q decidable: Dec(P) fact: (n)! primrec: primrec(n;b;c) exp: i^n less_than': less_than'(a;b) nat_plus: + subtype_rel: A ⊆B le: A ≤ B prop: and: P ∧ Q top: Top exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A uimplies: supposing a ge: i ≥  false: False implies:  Q nat: member: t ∈ T uall: [x:A]. B[x] all: x:A. B[x] rev_uimplies: rev_uimplies(P;Q) guard: {T}
Lemmas referenced :  int_term_value_mul_lemma itermMultiply_wf nat_wf int_term_value_subtract_lemma int_formula_prop_not_lemma itermSubtract_wf intformnot_wf subtract_wf decidable__le le_wf false_wf nat_plus_wf fact_wf exp_wf2 less_than'_wf less_than_wf ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf full-omega-unsat nat_properties fact_unroll_1 exp_step exp_preserves_le le_functionality multiply_functionality_wrt_le le_weakening le_transitivity
Rules used in proof :  multiplyEquality unionElimination dependent_set_memberEquality equalitySymmetry equalityTransitivity axiomEquality applyEquality because_Cache independent_pairEquality productElimination independent_pairFormation sqequalRule voidEquality voidElimination isect_memberEquality dependent_functionElimination intEquality int_eqEquality lambdaEquality dependent_pairFormation independent_functionElimination approximateComputation independent_isectElimination natural_numberEquality intWeakElimination rename setElimination hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}n:\mBbbN{}.  ((n)!  \mleq{}  n\^{}n)



Date html generated: 2018_05_21-PM-01_05_00
Last ObjectModification: 2018_05_18-PM-04_16_45

Theory : num_thy_1


Home Index