Nuprl Lemma : p-distrib
∀[p:{2...}]. ∀[a,x,y:p-adics(p)]. ((a * x + y = a * x + a * y ∈ p-adics(p)) ∧ (x + y * a = x * a + y * a ∈ p-adics(p)))
Proof
Definitions occuring in Statement :
p-mul: x * y,
p-add: x + y,
p-adics: p-adics(p),
int_upper: {i...},
uall: ∀[x:A]. B[x],
and: P ∧ Q,
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{}[a,x,y:p-adics(p)]. ((a * x + y = a * x + a * y) \mwedge{} (x + y * a = x * a + y * a))
Date html generated:
2018_05_21-PM-03_20_58
Last ObjectModification:
2018_05_19-AM-08_18_07
Theory : rings_1
Home
Index