Nuprl Lemma : remainder_wfa

[a:ℤ]. ∀[n:ℤ-o].  (a rem n ∈ ℤ)


Proof




Definitions occuring in Statement :  int_nzero: -o uall: [x:A]. B[x] member: t ∈ T remainder: rem m int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int_nzero: -o nequal: a ≠ b ∈  not: ¬A implies:  Q uimplies: supposing a 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:
Lemmas referenced :  int_nzero_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
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut remainderEquality hypothesisEquality sqequalHypSubstitution setElimination thin rename hypothesis lemma_by_obid isectElimination lambdaFormation natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll axiomEquality equalityTransitivity equalitySymmetry because_Cache

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (a  rem  n  \mmember{}  \mBbbZ{})



Date html generated: 2016_05_14-AM-07_23_01
Last ObjectModification: 2016_01_14-PM-10_02_49

Theory : int_2


Home Index