### Nuprl Lemma : p-mul-assoc

`∀[p:{2...}]. ∀[x,y,z:p-adics(p)].  (x * y * z = x * y * z ∈ p-adics(p))`

Proof

Definitions occuring in Statement :  p-mul: `x * y` p-adics: `p-adics(p)` int_upper: `{i...}` uall: `∀[x:A]. B[x]` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` crng: `CRng` rng: `Rng` p-adic-ring: `ℤ(p)` ring_p: `IsRing(T;plus;zero;neg;times;one)` rng_car: `|r|` pi1: `fst(t)` rng_plus: `+r` pi2: `snd(t)` rng_zero: `0` rng_minus: `-r` rng_times: `*` rng_one: `1` monoid_p: `IsMonoid(T;op;id)` group_p: `IsGroup(T;op;id;inv)` bilinear: `BiLinear(T;pl;tm)` ident: `Ident(T;op;id)` assoc: `Assoc(T;op)` inverse: `Inverse(T;op;id;inv)` infix_ap: `x f y` comm: `Comm(T;op)` and: `P ∧ Q`
Lemmas referenced :  p-adic-ring_wf crng_properties rng_properties int_upper_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality equalityTransitivity equalitySymmetry applyLambdaEquality setElimination rename sqequalRule productElimination natural_numberEquality

Latex:
\mforall{}[p:\{2...\}].  \mforall{}[x,y,z:p-adics(p)].    (x  *  y  *  z  =  x  *  y  *  z)

Date html generated: 2018_05_21-PM-03_20_51
Last ObjectModification: 2018_05_19-AM-08_18_11

Theory : rings_1

Home Index