Nuprl Lemma : eqmod-zero

m:ℤ(m ≡ mod m)


Proof




Definitions occuring in Statement :  eqmod: a ≡ mod m all: x:A. B[x] natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] eqmod: a ≡ mod m divides: a exists: x:A. B[x] member: t ∈ T decidable: Dec(P) or: P ∨ Q uall: [x:A]. B[x] uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) false: False implies:  Q not: ¬A top: Top prop:
Lemmas referenced :  subtract_wf equal_wf int_formula_prop_wf int_term_value_mul_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermMultiply_wf itermConstant_wf itermVar_wf itermSubtract_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation dependent_pairFormation natural_numberEquality cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin because_Cache hypothesis unionElimination isectElimination independent_isectElimination lambdaEquality int_eqEquality hypothesisEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule computeAll multiplyEquality

Latex:
\mforall{}m:\mBbbZ{}.  (m  \mequiv{}  0  mod  m)



Date html generated: 2016_05_14-PM-04_22_04
Last ObjectModification: 2016_01_14-PM-11_39_35

Theory : num_thy_1


Home Index