Nuprl Lemma : div_unique3

∀a:ℤ. ∀n:ℤ-o.
  ∀[p:ℤ]
    uiff((a ÷ n) = p ∈ ℤ;∃r:ℤ
                          (|r| < |n|
                          ∧ (a = ((p * n) + r) ∈ ℤ)
                          ∧ ((0 ≤ a) ⇒ (0 ≤ r))
                          ∧ (0 < r ⇒ 0 < a)
                          ∧ (r < 0 ⇒ a < 0)))


Proof



Definitions occuring in Statement :  absval: |i|,  int_nzero: ℤ-o,  less_than: a < b,  uiff: uiff(P;Q),  uall: ∀[x:A]. B[x],  le: A ≤ B,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  divide: n ÷ m,  multiply: n * m,  add: n + m,  natural_number: $n,  int: ℤ,  equal: s = t ∈ T
Definitions unfolded in proof :  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  uiff: uiff(P;Q),  and: P ∧ Q,  uimplies: b supposing a,  member: t ∈ T,  subtype_rel: A ⊆r B,  int_nzero: ℤ-o,  so_lambda: λ2x.t[x],  so_apply: x[s],  exists: ∃x:A. B[x],  nat: ℕ,  implies: P ⇒ Q,  nequal: a ≠ b ∈ T ,  not: ¬A,  false: False,  sq_type: SQType(T),  guard: {T},  true: True,  squash: ↓T,  prop: ℙ,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  top: Top,  subtract: n - m,  decidable: Dec(P),  or: P ∨ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  less_than: a < b,  less_than': less_than'(a;b),  bfalse: ff,  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  assert: ↑b,  le: A ≤ B,  cand: A c∧ B,  ge: i ≥ j 
Lemmas referenced :  set_subtype_base,  nequal_wf,  int_subtype_base,  istype-less_than,  absval_wf,  istype-le,  int_nzero_wf,  istype-int,  rem_bounds_absval,  subtype_base_sq,  equal_wf,  squash_wf,  true_wf,  istype-universe,  div_rem_sum,  subtype_rel_self,  iff_weakening_equal,  rem-sign,  istype-void,  mul-commutes,  add-commutes,  mul-distributes-right,  minus-one-mul,  mul-associates,  add-associates,  add-mul-special,  zero-mul,  zero-add,  minus-one-mul-top,  add-swap,  decidable__int_equal,  nat_wf,  le_wf,  absval-non-neg,  subtract_wf,  absval_sym,  minus-add,  minus-zero,  minus-minus,  add-zero,  absval_unfold2,  lt_int_wf,  eqtt_to_assert,  assert_of_lt_int,  istype-top,  eqff_to_assert,  bool_cases_sqequal,  bool_subtype_base,  iff_transitivity,  assert_wf,  bnot_wf,  not_wf,  less_than_wf,  iff_weakening_uiff,  assert_of_bnot,  istype-assert,  bool_wf,  not-equal-2,  add_functionality_wrt_le,  le-add-cancel,  not-lt-2,  condition-implies-le,  add_functionality_wrt_lt,  le_reflexive,  decidable__lt,  istype-false,  less-iff-le,  one-mul,  two-mul,  less_than_transitivity2,  le_weakening2,  minus-is-int-iff,  absval_mul,  mul_preserves_le,  multiply-is-int-iff,  le_antisymmetry_iff,  nat_properties,  decidable__le,  not-le-2,  le-add-cancel2,  less_than_transitivity1,  le_weakening,  less_than_irreflexivity
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  Error :lambdaFormation_alt,  Error :isect_memberFormation_alt,  independent_pairFormation,  cut,  introduction,  axiomEquality,  hypothesis,  thin,  rename,  Error :equalityIsType4,  Error :inhabitedIsType,  hypothesisEquality,  sqequalRule,  baseApply,  closedConclusion,  baseClosed,  applyEquality,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  intEquality,  Error :lambdaEquality_alt,  natural_numberEquality,  independent_isectElimination,  Error :productIsType,  setElimination,  equalityTransitivity,  equalitySymmetry,  Error :functionIsType,  because_Cache,  Error :universeIsType,  Error :dependent_pairFormation_alt,  remainderEquality,  independent_functionElimination,  voidElimination,  dependent_functionElimination,  promote_hyp,  instantiate,  cumulativity,  imageElimination,  universeEquality,  imageMemberEquality,  productElimination,  divideEquality,  Error :isect_memberEquality_alt,  multiplyEquality,  addEquality,  minusEquality,  unionElimination,  Error :dependent_set_memberEquality_alt,  equalityElimination,  lessCases,  axiomSqEquality,  Error :isectIsTypeImplies,  Error :equalityIsType1,  applyLambdaEquality
Latex:
\mforall{}a:\mBbbZ{}.  \mforall{}n:\mBbbZ{}\msupminus{}\msupzero{}.
    \mforall{}[p:\mBbbZ{}]
        uiff((a  \mdiv{}  n)  =  p;\mexists{}r:\mBbbZ{}
                                            (|r|  <  |n|
                                            \mwedge{}  (a  =  ((p  *  n)  +  r))
                                            \mwedge{}  ((0  \mleq{}  a)  {}\mRightarrow{}  (0  \mleq{}  r))
                                            \mwedge{}  (0  <  r  {}\mRightarrow{}  0  <  a)
                                            \mwedge{}  (r  <  0  {}\mRightarrow{}  a  <  0)))


Date html generated: 2019_06_20-AM-11_24_53
Last ObjectModification: 2018_10_18-PM-03_54_42

Theory : arithmetic


Home Index