### Nuprl Lemma : rem_to_div

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

Proof

Definitions occuring in Statement :  int_nzero: `ℤ-o` uall: `∀[x:A]. B[x]` remainder: `n rem m` divide: `n ÷ m` multiply: `n * m` subtract: `n - m` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` subtype_rel: `A ⊆r B` top: `Top` subtract: `n - m`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality addEquality hypothesis minusEquality multiplyEquality divideEquality setElimination rename lambdaFormation independent_functionElimination voidElimination intEquality natural_numberEquality because_Cache sqequalRule applyEquality lambdaEquality isect_memberEquality voidEquality remainderEquality equalitySymmetry axiomEquality

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

Date html generated: 2016_05_13-PM-03_35_22
Last ObjectModification: 2015_12_26-AM-09_43_10

Theory : arithmetic

Home Index