### Nuprl Lemma : divrem_wf

`∀[a:ℤ]. ∀[n:ℤ-o].  (divrem(a; n) ∈ ℤ × ℤ)`

Proof

Definitions occuring in Statement :  int_nzero: `ℤ-o` uall: `∀[x:A]. B[x]` member: `t ∈ T` product: `x:A × B[x]` divrem: `divrem(n; m)` int: `ℤ`
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` subtype_rel: `A ⊆r B`
Lemmas referenced :  int_subtype_base int_nzero_wf istype-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :divremEquality,  hypothesisEquality sqequalHypSubstitution setElimination thin rename cut hypothesis Error :lambdaFormation_alt,  independent_functionElimination voidElimination Error :equalityIstype,  Error :inhabitedIsType,  applyEquality introduction extract_by_obid sqequalRule baseClosed sqequalBase equalitySymmetry Error :universeIsType

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

Date html generated: 2019_06_20-AM-11_23_35
Last ObjectModification: 2019_03_27-PM-03_12_35

Theory : arithmetic

Home Index