Nuprl Lemma : divide-exact
∀[g:ℤ-o]. ∀[v:ℤ]. (((g * v) ÷ g) = v ∈ ℤ)
Proof
Definitions occuring in Statement :
int_nzero: ℤ-o,
uall: ∀[x:A]. B[x],
divide: n ÷ m,
multiply: n * m,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
int_nzero: ℤ-o,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
int_nzero_wf,
istype-int,
div-cancel-1,
mul-commutes
Rules used in proof :
universeIsType,
inhabitedIsType,
isectIsTypeImplies,
axiomEquality,
isect_memberEquality_alt,
dependent_functionElimination,
Error :memTop,
hypothesis,
hypothesisEquality,
rename,
setElimination,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
sqequalRule,
cut,
introduction,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[g:\mBbbZ{}\msupminus{}\msupzero{}]. \mforall{}[v:\mBbbZ{}]. (((g * v) \mdiv{} g) = v)
Date html generated:
2020_05_19-PM-09_35_37
Last ObjectModification:
2019_12_26-AM-11_45_14
Theory : arithmetic
Home
Index