Nuprl Lemma : p-minus-int

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


Proof




Definitions occuring in Statement :  p-int: k(p) p-minus: -(x) p-adics: p-adics(p) nat_plus: + uall: [x:A]. B[x] minus: -n 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-minus: -(x) 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-minus_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 minus_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 minusEquality 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:\mBbbZ{}].    (-(k(p))  =  -k(p))



Date html generated: 2018_05_21-PM-03_19_01
Last ObjectModification: 2018_05_19-AM-08_10_00

Theory : rings_1


Home Index