Nuprl Lemma : pa-mul_wf

[p:{2...}]. ∀[x,y:basic-padic(p)].  (pa-mul(p;x;y) ∈ padic(p))


Proof




Definitions occuring in Statement :  pa-mul: pa-mul(p;x;y) padic: padic(p) basic-padic: basic-padic(p) int_upper: {i...} uall: [x:A]. B[x] member: t ∈ T natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T pa-mul: pa-mul(p;x;y) nat_plus: + int_upper: {i...} le: A ≤ B and: P ∧ Q all: x:A. B[x] decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q not: ¬A rev_implies:  Q implies:  Q false: False prop: uiff: uiff(P;Q) uimplies: supposing a subtype_rel: A ⊆B top: Top less_than': less_than'(a;b) true: True
Lemmas referenced :  bpa-norm_wf_padic decidable__lt false_wf not-lt-2 add_functionality_wrt_le add-commutes zero-add le-add-cancel less_than_wf bpa-mul_wf basic-padic_wf int_upper_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin dependent_set_memberEquality setElimination rename because_Cache hypothesis productElimination dependent_functionElimination natural_numberEquality hypothesisEquality unionElimination independent_pairFormation lambdaFormation voidElimination independent_functionElimination independent_isectElimination applyEquality lambdaEquality isect_memberEquality voidEquality intEquality axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[p:\{2...\}].  \mforall{}[x,y:basic-padic(p)].    (pa-mul(p;x;y)  \mmember{}  padic(p))



Date html generated: 2018_05_21-PM-03_26_55
Last ObjectModification: 2018_05_19-AM-08_23_58

Theory : rings_1


Home Index