### Nuprl Lemma : p-reduce_wf

`∀[p:ℕ+]. ∀[n:ℕ]. ∀[i:ℤ].  (i mod(p^n) ∈ ℕp^n)`

Proof

Definitions occuring in Statement :  p-reduce: `i mod(p^n)` exp: `i^n` int_seg: `{i..j-}` nat_plus: `ℕ+` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` p-reduce: `i mod(p^n)` subtype_rel: `A ⊆r B` nat_plus: `ℕ+`
Lemmas referenced :  modulus_wf_int_mod exp_wf_nat_plus int-subtype-int_mod exp_wf2 nat_wf nat_plus_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality setElimination rename axiomEquality equalityTransitivity equalitySymmetry intEquality isect_memberEquality because_Cache

Latex:
\mforall{}[p:\mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbZ{}].    (i  mod(p\^{}n)  \mmember{}  \mBbbN{}p\^{}n)

Date html generated: 2018_05_21-PM-03_17_51
Last ObjectModification: 2018_05_19-AM-08_08_48

Theory : rings_1

Home Index