Nuprl Lemma : add_zero_int_mod

[n:ℤ]. ∀[x:ℤ_n].  ((x 0) x ∈ ℤ_n)


Proof




Definitions occuring in Statement :  int_mod: _n uall: [x:A]. B[x] add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int_mod: _n quotient: x,y:A//B[x; y] and: P ∧ Q all: x:A. B[x] implies:  Q prop: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a
Lemmas referenced :  eqmod_wf equal_wf equal-wf-base int_mod_wf quotient-member-eq eqmod_equiv_rel add-zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality because_Cache sqequalRule pertypeElimination productElimination thin equalityTransitivity hypothesis equalitySymmetry intEquality lambdaFormation rename extract_by_obid isectElimination hypothesisEquality dependent_functionElimination independent_functionElimination productEquality isect_memberEquality axiomEquality lambdaEquality independent_isectElimination addEquality natural_numberEquality

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[x:\mBbbZ{}\_n].    ((x  +  0)  =  x)



Date html generated: 2017_04_17-AM-09_47_38
Last ObjectModification: 2017_02_27-PM-05_44_31

Theory : num_thy_1


Home Index