### Nuprl Lemma : p-int-eventually-constant

`∀p:{2...}. ∀k:ℕ.  ∃n:ℕ+. ∀m:{n...}. ((k(p) m) = k ∈ ℤ)`

Proof

Definitions occuring in Statement :  p-int: `k(p)` int_upper: `{i...}` nat_plus: `ℕ+` nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` apply: `f a` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` sq_type: `SQType(T)` implies: `P `` Q` guard: `{T}` exists: `∃x:A. B[x]` nat_plus: `ℕ+` int_upper: `{i...}` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` prop: `ℙ` false: `False` and: `P ∧ Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` le: `A ≤ B` cand: `A c∧ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` less_than': `less_than'(a;b)` true: `True` squash: `↓T` rev_uimplies: `rev_uimplies(P;Q)` p-int: `k(p)` p-reduce: `i mod(p^n)` int_seg: `{i..j-}` lelt: `i ≤ j < k` less_than: `a < b` sq_stable: `SqStable(P)`
Lemmas referenced :  istype-nat istype-int_upper decidable__equal_int subtype_base_sq int_subtype_base nat_properties int_upper_properties decidable__lt full-omega-unsat intformnot_wf intformless_wf itermConstant_wf istype-int int_formula_prop_not_lemma istype-void int_formula_prop_less_lemma int_term_value_constant_lemma int_formula_prop_wf istype-less_than exp-positive intformand_wf itermVar_wf intformle_wf int_formula_prop_and_lemma int_term_value_var_lemma int_formula_prop_le_lemma exp_wf2 nat_plus_properties decidable__le istype-le log_wf add_nat_plus subtype_rel_sets_simple le_wf less_than_wf istype-false not-lt-2 add_functionality_wrt_le add-commutes le-add-cancel2 add-is-int-iff itermAdd_wf intformeq_wf int_term_value_add_lemma int_formula_prop_eq_lemma false_wf log-property squash_wf true_wf exp_add subtype_rel_self iff_weakening_equal exp1 upper_subtype_nat less_than_functionality le_weakening multiply_functionality_wrt_le mul_preserves_lt itermMultiply_wf int_term_value_mul_lemma set_subtype_base modulus_base exp_wf_nat_plus exp-nondecreasing nat_plus_subtype_nat sq_stable__le le_weakening2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin natural_numberEquality dependent_functionElimination setElimination rename hypothesisEquality unionElimination instantiate cumulativity intEquality independent_isectElimination because_Cache independent_functionElimination dependent_pairFormation_alt dependent_set_memberEquality_alt approximateComputation lambdaEquality_alt isect_memberEquality_alt voidElimination sqequalRule universeIsType equalityTransitivity equalitySymmetry int_eqEquality independent_pairFormation addEquality applyEquality inhabitedIsType productElimination applyLambdaEquality pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed equalityIstype imageElimination imageMemberEquality universeEquality multiplyEquality functionIsType sqequalBase productIsType

Latex:
\mforall{}p:\{2...\}.  \mforall{}k:\mBbbN{}.    \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\{n...\}.  ((k(p)  m)  =  k)

Date html generated: 2019_10_15-AM-10_34_25
Last ObjectModification: 2019_02_11-PM-02_03_22

Theory : rings_1

Home Index