### Nuprl Lemma : rem-mul

`∀[a:ℤ]. ∀[n,m:ℤ-o].  ((a * n rem m * n) = ((a rem m) * n) ∈ ℤ)`

Proof

Definitions occuring in Statement :  int_nzero: `ℤ-o` uall: `∀[x:A]. B[x]` remainder: `n rem m` multiply: `n * m` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` int_nzero: `ℤ-o` uimplies: `b supposing a` nequal: `a ≠ b ∈ T ` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` all: `∀x:A. B[x]` top: `Top` and: `P ∧ Q` prop: `ℙ` decidable: `Dec(P)` or: `P ∨ Q` uiff: `uiff(P;Q)`
Lemmas referenced :  false_wf int_term_value_add_lemma int_term_value_mul_lemma itermAdd_wf itermMultiply_wf multiply-is-int-iff add-is-int-iff decidable__equal_int mul-swap mul-distributes mul-commutes mul_preserves_eq nequal_wf equal_wf int_formula_prop_wf int_formula_prop_not_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformnot_wf itermConstant_wf itermVar_wf intformeq_wf intformand_wf satisfiable-full-omega-tt int_nzero_properties int_entire_a div_rem_sum int_nzero_wf div-mul-cancel
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality intEquality multiplyEquality setElimination rename dependent_set_memberEquality independent_isectElimination lambdaFormation natural_numberEquality dependent_pairFormation lambdaEquality int_eqEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll equalityTransitivity equalitySymmetry divideEquality because_Cache unionElimination pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed productElimination

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n,m:\mBbbZ{}\msupminus{}\msupzero{}].    ((a  *  n  rem  m  *  n)  =  ((a  rem  m)  *  n))

Date html generated: 2016_05_14-AM-07_24_55
Last ObjectModification: 2016_01_14-PM-10_01_39

Theory : int_2

Home Index