Nuprl Lemma : div_minus

[a:ℤ]. ∀[b:ℤ-o].  (((-a) ÷ -b) (a ÷ b) ∈ ℤ)


Proof




Definitions occuring in Statement :  int_nzero: -o uall: [x:A]. B[x] divide: n ÷ m minus: -n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nequal: a ≠ b ∈  not: ¬A implies:  Q int_nzero: -o all: x:A. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a or: P ∨ Q guard: {T} subtract: m subtype_rel: A ⊆B top: Top le: A ≤ B less_than': less_than'(a;b) true: True false: False prop: squash: T iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  not-equal-2 le_antisymmetry_iff condition-implies-le minus-zero add-zero add-associates minus-add minus-minus minus-one-mul zero-add minus-one-mul-top two-mul add-commutes mul-distributes-right one-mul add_functionality_wrt_le le-add-cancel add-swap add-mul-special equal-wf-T-base int_nzero_wf equal_wf squash_wf true_wf div_anti_sym subtype_rel_self iff_weakening_equal div_anti_sym2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation addEquality hypothesis because_Cache sqequalHypSubstitution setElimination thin rename extract_by_obid dependent_functionElimination hypothesisEquality natural_numberEquality productElimination independent_isectElimination unionElimination isectElimination minusEquality sqequalRule applyEquality lambdaEquality isect_memberEquality voidElimination voidEquality multiplyEquality independent_functionElimination baseClosed axiomEquality intEquality imageElimination equalityTransitivity equalitySymmetry universeEquality divideEquality imageMemberEquality instantiate

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



Date html generated: 2019_06_20-AM-11_25_12
Last ObjectModification: 2018_08_18-PM-00_47_28

Theory : arithmetic


Home Index