### Nuprl Lemma : p-reduce-0

`∀p:ℕ+. ∀n:ℕ.  (0 mod(p^n) = 0 ∈ ℤ)`

Proof

Definitions occuring in Statement :  p-reduce: `i mod(p^n)` nat_plus: `ℕ+` nat: `ℕ` all: `∀x:A. B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` p-reduce: `i mod(p^n)` uall: `∀[x:A]. B[x]` member: `t ∈ T` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` prop: `ℙ` nat_plus: `ℕ+`
Lemmas referenced :  modulus_base exp_wf_nat_plus false_wf exp-positive-stronger lelt_wf exp_wf2 nat_wf nat_plus_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis dependent_set_memberEquality natural_numberEquality independent_pairFormation dependent_functionElimination setElimination rename because_Cache

Latex:
\mforall{}p:\mBbbN{}\msupplus{}.  \mforall{}n:\mBbbN{}.    (0  mod(p\^{}n)  =  0)

Date html generated: 2018_05_21-PM-03_18_00
Last ObjectModification: 2018_05_19-AM-08_08_58

Theory : rings_1

Home Index