Nuprl Lemma : div_anti_sym

`∀[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: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nequal: `a ≠ b ∈ T ` not: `¬A` implies: `P `` Q` int_nzero: `ℤ-o` all: `∀x:A. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` or: `P ∨ Q` guard: `{T}` subtract: `n - m` subtype_rel: `A ⊆r B` top: `Top` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` false: `False` prop: `ℙ` decidable: `Dec(P)` nat: `ℕ` int_lower: `{...i}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` sq_type: `SQType(T)` nat_plus: `ℕ+`
Lemmas referenced :  int_nzero_wf 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 decidable__le div_4_to_1 le_wf false_wf not-le-2 le-add-cancel2 subtract_wf le_reflexive mul-associates zero-mul subtype_base_sq int_subtype_base div_3_to_1 div_2_to_1 decidable__lt not-lt-2 less_than_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality axiomEquality because_Cache intEquality lambdaFormation addEquality setElimination rename dependent_functionElimination natural_numberEquality productElimination independent_isectElimination unionElimination minusEquality applyEquality lambdaEquality voidElimination voidEquality multiplyEquality independent_functionElimination dependent_set_memberEquality divideEquality independent_pairFormation instantiate cumulativity equalityTransitivity equalitySymmetry

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

Date html generated: 2016_05_13-PM-03_36_14
Last ObjectModification: 2015_12_26-AM-09_44_01

Theory : arithmetic

Home Index