Nuprl Lemma : quot_rem

Nuprl Lemma : quot_rem_exists

∀a:ℤ. ∀b:ℕ⁺. ∃q:ℤ. ∃r:ℕb. (a = ((q * b) + r) ∈ ℤ)

Proof

Definitions occuring in Statement : int_seg: {i..j^-}, nat_plus: ℕ⁺, all: ∀x:A. B[x], exists: ∃x:A. B[x], multiply: n * m, add: n + m, natural_number: $n, int: ℤ, equal: s = t ∈ T
Definitions unfolded in proof : all: ∀x:A. B[x], member: t ∈ T, decidable: Dec(P), or: P ∨ Q, nat: ℕ, uall: ∀[x:A]. B[x], prop: ℙ, exists: ∃x:A. B[x], nat_plus: ℕ⁺, subtype_rel: A ⊆r B, int_seg: {i..j^-}, uimplies: b supposing a, not: ¬A, implies: P ⇒ Q, satisfiable_int_formula: satisfiable_int_formula(fmla), false: False, top: Top, and: P ∧ Q, lelt: i ≤ j < k, le: A ≤ B, less_than': less_than'(a;b), guard: {T}, ge: i ≥ j , subtract: n - m
Lemmas referenced : nat_plus_wf, istype-int, decidable__le, quot_rem_exists_n, le_wf, int_seg_wf, int_subtype_base, nat_plus_properties, full-omega-unsat, intformand_wf, intformnot_wf, intformle_wf, itermConstant_wf, itermMinus_wf, itermVar_wf, int_formula_prop_and_lemma, istype-void, int_formula_prop_not_lemma, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_minus_lemma, int_term_value_var_lemma, int_formula_prop_wf, decidable__equal_int, istype-false, int_seg_properties, nat_properties, decidable__lt, intformless_wf, intformeq_wf, int_formula_prop_less_lemma, int_formula_prop_eq_lemma, less_than_wf, itermAdd_wf, itermMultiply_wf, int_term_value_add_lemma, int_term_value_mul_lemma, subtract_wf, itermSubtract_wf, int_term_value_subtract_lemma, minus-add, mul-distributes-right, add-associates, minus-one-mul, mul-associates, mul-commutes, add-swap, add-commutes, add-mul-special, zero-mul, zero-add
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :lambdaFormation_alt, Error :universeIsType, cut, introduction, extract_by_obid, hypothesis, sqequalHypSubstitution, dependent_functionElimination, thin, natural_numberEquality, hypothesisEquality, unionElimination, Error :dependent_set_memberEquality_alt, isectElimination, productElimination, Error :dependent_pairFormation_alt, setElimination, rename, sqequalRule, Error :productIsType, Error :equalityIsType4, Error :inhabitedIsType, applyEquality, addEquality, multiplyEquality, because_Cache, minusEquality, independent_isectElimination, approximateComputation, independent_functionElimination, Error :lambdaEquality_alt, int_eqEquality, Error :isect_memberEquality_alt, voidElimination, independent_pairFormation, equalityTransitivity, equalitySymmetry

Latex:
\mforall{}a:\mBbbZ{}. \mforall{}b:\mBbbN{}\msupplus{}. \mexists{}q:\mBbbZ{}. \mexists{}r:\mBbbN{}b. (a = ((q * b) + r)) Date html generated: 2019_06_20-PM-02_22_13 Last ObjectModification: 2018_10_05-PM-05_45_41 Theory : num_thy_1 Home Index