### Nuprl Lemma : div-mul-cancel2

`∀[a:ℤ]. ∀[n,m:ℤ-o].  ((n * a) ÷ n * m ~ a ÷ m)`

Proof

Definitions occuring in Statement :  int_nzero: `ℤ-o` uall: `∀[x:A]. B[x]` divide: `n ÷ m` multiply: `n * m` int: `ℤ` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` sq_type: `SQType(T)` all: `∀x:A. B[x]` implies: `P `` Q` guard: `{T}`
Lemmas referenced :  subtype_base_sq int_subtype_base mul-commutes div-mul-cancel trivial-equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination cumulativity intEquality independent_isectElimination hypothesis sqequalRule because_Cache dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination axiomSqEquality isect_memberEquality_alt hypothesisEquality isectIsTypeImplies inhabitedIsType

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

Date html generated: 2020_05_19-PM-09_41_14
Last ObjectModification: 2019_12_28-AM-11_28_39

Theory : int_2

Home Index