### Nuprl Lemma : divrem-sq

`∀[a:ℤ]. ∀[n:ℤ-o].  (divrem(a; n) ~ <a ÷ n, a rem n>)`

Proof

Definitions occuring in Statement :  int_nzero: `ℤ-o` uall: `∀[x:A]. B[x]` pair: `<a, b>` remainder: `n rem m` divide: `n ÷ m` divrem: `divrem(n; m)` int: `ℤ` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` remainder: `n rem m` divide: `n ÷ m` all: `∀x:A. B[x]` implies: `P `` Q`
Lemmas referenced :  divrem_wf int_nzero_wf istype-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis Error :inhabitedIsType,  Error :lambdaFormation_alt,  productElimination sqequalRule Error :equalityIstype,  equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination axiomSqEquality Error :universeIsType,  Error :isect_memberEquality_alt,  Error :isectIsTypeImplies

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (divrem(a;  n)  \msim{}  <a  \mdiv{}  n,  a  rem  n>)

Date html generated: 2019_06_20-AM-11_23_37
Last ObjectModification: 2019_03_06-AM-10_46_56

Theory : arithmetic

Home Index