Nuprl Lemma : add_eqmod_zero

m,x,y:ℤ.  ((x ≡ mod m)  (y ≡ mod m)  ((x y) ≡ mod m))


Proof




Definitions occuring in Statement :  eqmod: a ≡ mod m all: x:A. B[x] implies:  Q add: m natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] top: Top squash: T true: True
Lemmas referenced :  eqmod_wf add-commutes zero-add add_functionality_wrt_eqmod
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality natural_numberEquality hypothesis intEquality sqequalRule isect_memberEquality voidElimination voidEquality addEquality because_Cache applyEquality lambdaEquality imageElimination imageMemberEquality baseClosed equalitySymmetry hyp_replacement Error :applyLambdaEquality,  dependent_functionElimination independent_functionElimination

Latex:
\mforall{}m,x,y:\mBbbZ{}.    ((x  \mequiv{}  0  mod  m)  {}\mRightarrow{}  (y  \mequiv{}  0  mod  m)  {}\mRightarrow{}  ((x  +  y)  \mequiv{}  0  mod  m))



Date html generated: 2016_10_21-AM-11_09_07
Last ObjectModification: 2016_07_12-AM-06_01_37

Theory : num_thy_1


Home Index