### Nuprl Lemma : div_2_to_1

[a:{...0}]. ∀[b:ℕ+].  ((a ÷ b) (-((-a) ÷ b)) ∈ ℤ)

Proof

Definitions occuring in Statement :  int_lower: {...i} nat_plus: + uall: [x:A]. B[x] divide: n ÷ m minus: -n natural_number: \$n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat_plus: + int_lower: {...i} uimplies: supposing a all: x:A. B[x] top: Top int_nzero: -o and: P ∧ Q le: A ≤ B cand: c∧ B less_than: a < b squash: T nequal: a ≠ b ∈  not: ¬A implies:  Q false: False guard: {T} subtype_rel: A ⊆B prop: uiff: uiff(P;Q) nat: exists: x:A. B[x] true: True iff: ⇐⇒ Q rev_implies:  Q less_than': less_than'(a;b) sq_type: SQType(T) subtract: m
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename natural_numberEquality minusEquality because_Cache independent_isectElimination dependent_functionElimination Error :universeIsType,  sqequalRule Error :isect_memberEquality_alt,  axiomEquality Error :isectIsTypeImplies,  Error :inhabitedIsType,  multiplyEquality voidElimination Error :dependent_set_memberEquality_alt,  independent_pairFormation productElimination imageElimination Error :lambdaFormation_alt,  equalityTransitivity equalitySymmetry independent_functionElimination Error :equalityIstype,  applyEquality baseClosed sqequalBase intEquality divideEquality Error :dependent_pairFormation_alt,  remainderEquality Error :productIsType,  Error :lambdaEquality_alt,  baseApply closedConclusion Error :functionIsType,  imageMemberEquality lambdaFormation voidEquality isect_memberEquality lambdaEquality cumulativity instantiate addEquality dependent_set_memberEquality

Latex:
\mforall{}[a:\{...0\}].  \mforall{}[b:\mBbbN{}\msupplus{}].    ((a  \mdiv{}  b)  =  (-((-a)  \mdiv{}  b)))

Date html generated: 2019_06_20-AM-11_25_00
Last ObjectModification: 2019_01_04-PM-06_13_14

Theory : arithmetic

Home Index