Nuprl Lemma : p-mul-comm

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


Proof




Definitions occuring in Statement :  p-mul: y p-adics: p-adics(p) int_upper: {i...} uall: [x:A]. B[x] natural_number: $n equal: 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: y comm: Comm(T;op)
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 natural_numberEquality

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



Date html generated: 2018_05_21-PM-03_21_01
Last ObjectModification: 2018_05_19-AM-08_18_18

Theory : rings_1


Home Index