### Nuprl Lemma : pa-mul_functionality

(pa-mul(p;x1;y1) pa-mul(q;x2;y2) ∈ padic(p)) supposing ((p q ∈ ℤand bpa-equiv(p;x1;x2) and bpa-equiv(p;y1;y2))

Proof

Definitions occuring in Statement :  pa-mul: pa-mul(p;x;y) padic: padic(p) bpa-equiv: bpa-equiv(p;x;y) basic-padic: basic-padic(p) int_upper: {i...} uimplies: supposing a uall: [x:A]. B[x] natural_number: \$n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T sq_type: SQType(T) all: x:A. B[x] implies:  Q guard: {T} uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) pa-mul: pa-mul(p;x;y) nat_plus: + int_upper: {i...} le: A ≤ B decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q not: ¬A rev_implies:  Q false: False prop: subtype_rel: A ⊆B less_than': less_than'(a;b) true: True basic-padic: basic-padic(p) bpa-equiv: bpa-equiv(p;x;y) bpa-mul: bpa-mul(p;x;y) top: Top nat: squash: T ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] p-adics: p-adics(p) so_lambda: λ2x.t[x] subtract: m int_seg: {i..j-} lelt: i ≤ j < k so_apply: x[s]
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity intEquality independent_isectElimination hypothesis dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination hypothesisEquality productElimination dependent_set_memberEquality setElimination rename because_Cache natural_numberEquality unionElimination independent_pairFormation lambdaFormation voidElimination sqequalRule applyEquality lambdaEquality isect_memberEquality voidEquality imageElimination universeEquality imageMemberEquality baseClosed hyp_replacement addEquality approximateComputation dependent_pairFormation int_eqEquality minusEquality applyLambdaEquality

Latex:
(pa-mul(p;x1;y1)  =  pa-mul(q;x2;y2))  supposing
((p  =  q)  and
bpa-equiv(p;x1;x2)  and
bpa-equiv(p;y1;y2))

Date html generated: 2018_05_21-PM-03_27_00
Last ObjectModification: 2018_05_19-AM-08_24_23

Theory : rings_1

Home Index