Nuprl Lemma : p-add-int

[p:ℕ+]. ∀[k,j:ℤ].  (k(p) j(p) j(p) ∈ p-adics(p))


Proof




Definitions occuring in Statement :  p-int: k(p) p-add: y p-adics: p-adics(p) nat_plus: + uall: [x:A]. B[x] add: m int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) uimplies: supposing a p-int: k(p) p-add: y p-reduce: mod(p^n) subtype_rel: A ⊆B nat_plus: + int_seg: {i..j-} implies:  Q iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  p-adics-equal p-add_wf p-int_wf nat_plus_wf exp_wf2 nat_plus_subtype_nat modulus_wf_int_mod exp_wf_nat_plus int-subtype-int_mod int_seg_wf eqmod_functionality_wrt_eqmod eqmod_transitivity mod-eqmod add_functionality_wrt_eqmod eqmod_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination hypothesis addEquality productElimination independent_isectElimination lambdaFormation sqequalRule intEquality isect_memberEquality axiomEquality because_Cache applyEquality setElimination rename lambdaEquality natural_numberEquality independent_functionElimination

Latex:
\mforall{}[p:\mBbbN{}\msupplus{}].  \mforall{}[k,j:\mBbbZ{}].    (k(p)  +  j(p)  =  k  +  j(p))



Date html generated: 2018_05_21-PM-03_18_53
Last ObjectModification: 2018_05_19-AM-08_09_54

Theory : rings_1


Home Index