Nuprl Lemma : exp-greater

[x:{2...}]. ∀[n:ℕ].  n < x^n


Proof




Definitions occuring in Statement :  exp: i^n int_upper: {i...} nat: less_than: a < b uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A all: x:A. B[x] top: Top and: P ∧ Q prop: guard: {T} int_upper: {i...} less_than: a < b squash: T less_than': less_than'(a;b) true: True decidable: Dec(P) or: P ∨ Q nat_plus: + le: A ≤ B iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) subtype_rel: A ⊆B sq_type: SQType(T) subtract: m so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf member-less_than exp_wf2 int_upper_properties exp0_lemma le_wf decidable__le subtract_wf intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma exp_step mul_preserves_lt decidable__lt false_wf not-lt-2 add_functionality_wrt_le add-commutes zero-add le-add-cancel decidable__equal_int subtype_base_sq int_subtype_base itermMultiply_wf int_term_value_mul_lemma not-equal-2 less-iff-le add-associates add-zero le-add-cancel2 condition-implies-le minus-add add-swap minus-minus minus-one-mul minus-one-mul-top nat_plus_wf equal_wf subtract-add-cancel nat_wf int_upper_wf nat_plus_properties itermAdd_wf int_term_value_add_lemma primrec-wf-nat-plus
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll independent_functionElimination imageMemberEquality baseClosed dependent_set_memberEquality because_Cache unionElimination productElimination applyEquality instantiate cumulativity equalityTransitivity equalitySymmetry multiplyEquality addEquality minusEquality imageElimination

Latex:
\mforall{}[x:\{2...\}].  \mforall{}[n:\mBbbN{}].    n  <  x\^{}n



Date html generated: 2017_04_17-AM-09_45_07
Last ObjectModification: 2017_02_27-PM-05_39_23

Theory : num_thy_1


Home Index