### Nuprl Lemma : div_rem_sum2

`∀[a:ℤ]. ∀[n:ℤ-o].  (n * (a ÷ n) ~ a - a rem 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: `ℤ` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` int_nzero: `ℤ-o` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a`
Lemmas referenced :  div_rem_sum int_nzero_wf int_subtype_base set_subtype_base nequal_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality intEquality because_Cache hyp_replacement equalitySymmetry Error :applyLambdaEquality,  sqequalIntensionalEquality applyEquality sqequalRule baseApply closedConclusion baseClosed lambdaEquality natural_numberEquality independent_isectElimination

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

Date html generated: 2016_10_21-AM-09_58_38
Last ObjectModification: 2016_07_12-AM-05_12_38

Theory : int_2

Home Index