Nuprl Lemma : less-efficient-exp

i:ℤ. ∀n:ℕ.  (∃j:{ℤ(j i^n ∈ ℤ)})


Proof




Definitions occuring in Statement :  exp: i^n nat: all: x:A. B[x] sq_exists: x:{A| B[x]} int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T nat: decidable: Dec(P) or: P ∨ Q uall: [x:A]. B[x] uimplies: supposing a sq_type: SQType(T) guard: {T} prop: so_lambda: λ2x.t[x] subtype_rel: A ⊆B le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A so_apply: x[s] sq_exists: x:{A| B[x]} so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] iff: ⇐⇒ Q rev_implies:  Q top: Top nat_plus: + less_than: a < b squash: T true: True ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] int_seg: {i..j-} lelt: i ≤ j < k int_nzero: -o nequal: a ≠ b ∈  uiff: uiff(P;Q)
Lemmas referenced :  decidable__equal_int subtype_base_sq int_subtype_base all_wf int_seg_wf sq_exists_wf equal-wf-base-T exp_wf2 int_seg_subtype_nat false_wf nat_wf natrec_wf exp1 iff_weakening_equal equal-wf-base exp0_lemma div_bounds_1 less_than_wf div_mono1 le_wf nat_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf intformeq_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_le_lemma int_formula_prop_wf lelt_wf mul_bounds_1a divide_wf exp_add remainder_wf equal_wf squash_wf true_wf div_rem_sum nequal_wf add-is-int-iff itermAdd_wf itermMultiply_wf int_term_value_add_lemma int_term_value_mul_lemma decidable__le multiply-is-int-iff two-mul mul-commutes rem_bounds_1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename because_Cache hypothesis natural_numberEquality unionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination independent_functionElimination hypothesisEquality sqequalRule lambdaEquality applyEquality independent_pairFormation functionExtensionality functionEquality dependent_set_memberFormation equalityEquality equalityTransitivity equalitySymmetry productElimination baseApply closedConclusion baseClosed isect_memberEquality voidElimination voidEquality dependent_set_memberEquality imageMemberEquality dependent_pairFormation int_eqEquality computeAll hyp_replacement imageElimination universeEquality addLevel addEquality remainderEquality pointwiseFunctionality promote_hyp multiplyEquality

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}n:\mBbbN{}.    (\mexists{}j:\{\mBbbZ{}|  (j  =  i\^{}n)\})



Date html generated: 2016_10_25-AM-11_00_06
Last ObjectModification: 2016_07_12-AM-07_07_31

Theory : general


Home Index