Nuprl Lemma : p-add_wf

[p:ℕ+]. ∀[x,y:p-adics(p)].  (x y ∈ p-adics(p))


Proof




Definitions occuring in Statement :  p-add: y p-adics: p-adics(p) nat_plus: + uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T p-add: y p-adics: p-adics(p) subtype_rel: A ⊆B int_seg: {i..j-} nat_plus: + all: x:A. B[x] so_lambda: λ2x.t[x] decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q not: ¬A rev_implies:  Q implies:  Q false: False prop: uiff: uiff(P;Q) uimplies: supposing a subtract: m top: Top le: A ≤ B less_than': less_than'(a;b) true: True nat: guard: {T} satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] lelt: i ≤ j < k so_apply: x[s] int_upper: {i...}
Lemmas referenced :  p-reduce_wf nat_plus_subtype_nat int_seg_wf exp_wf2 nat_plus_wf all_wf eqmod_wf decidable__lt false_wf not-lt-2 less-iff-le condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel less_than_wf int_seg_properties nat_plus_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf p-adics_wf eqmod_functionality_wrt_eqmod eqmod_weakening p-reduce-eqmod p-reduce-eqmod-exp add_functionality_wrt_eqmod eqmod_inversion
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality lambdaEquality extract_by_obid isectElimination hypothesisEquality applyEquality hypothesis addEquality natural_numberEquality because_Cache lambdaFormation dependent_functionElimination unionElimination independent_pairFormation voidElimination productElimination independent_functionElimination independent_isectElimination isect_memberEquality voidEquality intEquality minusEquality approximateComputation dependent_pairFormation int_eqEquality equalityTransitivity equalitySymmetry applyLambdaEquality axiomEquality functionExtensionality

Latex:
\mforall{}[p:\mBbbN{}\msupplus{}].  \mforall{}[x,y:p-adics(p)].    (x  +  y  \mmember{}  p-adics(p))



Date html generated: 2018_05_21-PM-03_18_15
Last ObjectModification: 2018_05_19-AM-08_09_19

Theory : rings_1


Home Index