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

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

Proof

Definitions occuring in Statement :  p-int: `k(p)` exp: `i^n` int_upper: `{i...}` nat_plus: `ℕ+` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` apply: `f a` subtract: `n - m` minus: `-n` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` int_upper: `{i...}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` prop: `ℙ` implies: `P `` Q` le: `A ≤ B` and: `P ∧ Q` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` top: `Top` less_than': `less_than'(a;b)` true: `True` nat_plus: `ℕ+` guard: `{T}` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` nat: `ℕ` less_than: `a < b` squash: `↓T` p-int: `k(p)` p-reduce: `i mod(p^n)` p-adics: `p-adics(p)` int_seg: `{i..j-}` sq_stable: `SqStable(P)` lelt: `i ≤ j < k`
Lemmas referenced :  nat_plus_wf int_upper_wf log-property subtype_rel_sets le_wf less_than_wf decidable__lt false_wf not-lt-2 add_functionality_wrt_le add-commutes le-add-cancel2 nat_plus_subtype_nat nat_plus_properties int_upper_properties full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_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_wf log_wf nat_wf add_nat_plus add-is-int-iff itermAdd_wf intformeq_wf int_term_value_add_lemma int_formula_prop_eq_lemma equal_wf exp_wf2 all_wf p-int_wf zero-add le-add-cancel p-adics_wf less_than_transitivity1 int_seg_wf upper_subtype_nat sq_stable__le le_weakening2 subtract_wf exp-nondecreasing decidable__le intformle_wf int_formula_prop_le_lemma mod_bounds less_than_transitivity2 modulus_base_neg itermMinus_wf int_term_value_minus_lemma lelt_wf decidable__equal_int itermSubtract_wf int_term_value_subtract_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesisEquality applyEquality sqequalRule intEquality because_Cache lambdaEquality independent_isectElimination setElimination rename setEquality productElimination dependent_functionElimination unionElimination independent_pairFormation voidElimination independent_functionElimination isect_memberEquality voidEquality approximateComputation dependent_pairFormation int_eqEquality dependent_set_memberEquality addEquality imageMemberEquality baseClosed equalityTransitivity equalitySymmetry applyLambdaEquality pointwiseFunctionality promote_hyp baseApply closedConclusion minusEquality imageElimination

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

Date html generated: 2018_05_21-PM-03_19_12
Last ObjectModification: 2018_05_19-AM-08_10_18

Theory : rings_1

Home Index