### Nuprl Lemma : p-reduce-eqmod-exp

`∀p:ℕ+. ∀n:ℕ. ∀m:{n...}. ∀z:ℤ.  (z mod(p^m) ≡ z mod p^n)`

Proof

Definitions occuring in Statement :  p-reduce: `i mod(p^n)` eqmod: `a ≡ b mod m` exp: `i^n` int_upper: `{i...}` nat_plus: `ℕ+` nat: `ℕ` all: `∀x:A. B[x]` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` uimplies: `b supposing a` int_upper: `{i...}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` guard: `{T}` nat_plus: `ℕ+` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` and: `P ∧ Q` sq_type: `SQType(T)` p-reduce: `i mod(p^n)` label: `...\$L... t` uiff: `uiff(P;Q)` subtype_rel: `A ⊆r B` true: `True` squash: `↓T` int_seg: `{i..j-}` lelt: `i ≤ j < k` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` eqmod: `a ≡ b mod m` divides: `b | a` le: `A ≤ B` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T `
Lemmas referenced :  subtype_base_sq int_upper_wf set_subtype_base le_wf int_subtype_base int_upper_properties nat_properties nat_plus_properties decidable__equal_int subtract_wf full-omega-unsat intformnot_wf intformeq_wf itermVar_wf itermAdd_wf itermSubtract_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_subtract_lemma int_formula_prop_wf decidable__le intformand_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_le_lemma itermConstant_wf int_term_value_constant_lemma equal_wf nat_wf nat_plus_wf exp_wf2 multiply-is-int-iff itermMultiply_wf int_term_value_mul_lemma false_wf exp-positive-stronger less_than_wf int-subtype-int_mod eqmod_wf squash_wf true_wf modulus_wf_int_mod int_mod_wf exp_add int_seg_wf int_seg_properties subtype_rel_self iff_weakening_equal mod-eqmod mul_nat_plus exp_wf_nat_plus subtract-is-int-iff mod_bounds_1 mul_nzero exp_wf3 subtype_rel_sets nequal_wf intformless_wf int_formula_prop_less_lemma equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity setElimination rename because_Cache hypothesis independent_isectElimination sqequalRule lambdaEquality hypothesisEquality intEquality dependent_functionElimination addEquality unionElimination natural_numberEquality approximateComputation independent_functionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality dependent_set_memberEquality independent_pairFormation equalityTransitivity equalitySymmetry pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed productElimination applyEquality imageElimination imageMemberEquality applyLambdaEquality universeEquality multiplyEquality setEquality

Latex:
\mforall{}p:\mBbbN{}\msupplus{}.  \mforall{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  \mforall{}z:\mBbbZ{}.    (z  mod(p\^{}m)  \mequiv{}  z  mod  p\^{}n)

Date html generated: 2018_05_21-PM-03_18_06
Last ObjectModification: 2018_05_19-AM-08_09_10

Theory : rings_1

Home Index