Nuprl Lemma : div-cancel-1

`∀a:ℤ. ∀b:ℤ-o.  (((a * b) ÷ b) = a ∈ ℤ)`

Proof

Definitions occuring in Statement :  int_nzero: `ℤ-o` all: `∀x:A. B[x]` divide: `n ÷ m` multiply: `n * m` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` int_nzero: `ℤ-o` uall: `∀[x:A]. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` exists: `∃x:A. B[x]` cand: `A c∧ B` less_than: `a < b` squash: `↓T` implies: `P `` Q` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` subtype_rel: `A ⊆r B` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` absval: `|i|` nequal: `a ≠ b ∈ T `
Lemmas referenced :  div_unique3 add-zero istype-false istype-le istype-less_than absval_wf set_subtype_base nequal_wf int_subtype_base int_nzero_wf istype-int minus-zero absval-positive
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin multiplyEquality hypothesisEquality setElimination rename hypothesis isectElimination productElimination independent_isectElimination dependent_pairFormation_alt natural_numberEquality independent_pairFormation imageElimination sqequalRule because_Cache voidElimination productIsType applyEquality lambdaEquality_alt inhabitedIsType equalityTransitivity equalitySymmetry equalityIstype baseApply closedConclusion baseClosed intEquality sqequalBase functionIsType universeIsType independent_functionElimination

Latex:
\mforall{}a:\mBbbZ{}.  \mforall{}b:\mBbbZ{}\msupminus{}\msupzero{}.    (((a  *  b)  \mdiv{}  b)  =  a)

Date html generated: 2020_05_19-PM-09_35_31
Last ObjectModification: 2019_10_16-PM-02_00_08

Theory : arithmetic

Home Index