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