Nuprl Lemma : divides_iff_rem

Nuprl Lemma : divides_iff_rem_zero

∀a:ℤ. ∀b:ℤ^-^o. (b | a ⇐⇒ (a rem b) = 0 ∈ ℤ)

Proof

Definitions occuring in Statement : divides: b | a, int_nzero: ℤ^-^o, all: ∀x:A. B[x], iff: P ⇐⇒ Q, remainder: n rem m, natural_number: $n, int: ℤ, equal: s = t ∈ T
Definitions unfolded in proof : all: ∀x:A. B[x], iff: P ⇐⇒ Q, and: P ∧ Q, implies: P ⇒ Q, member: t ∈ T, uall: ∀[x:A]. B[x], int_nzero: ℤ^-^o, prop: ℙ, rev_implies: P ⇐ Q, subtype_rel: A ⊆r B, so_lambda: λ₂x.t[x], so_apply: x[s], uimplies: b supposing a, nat_plus: ℕ⁺, nat: ℕ, squash: ↓T, true: True, guard: {T}, exists: ∃x:A. B[x], div_nrel: Div(a;n;q), lelt: i ≤ j < k, divides: b | a, uiff: uiff(P;Q), less_than: a < b, cand: A c∧ B, le: A ≤ B, ge: i ≥ j , decidable: Dec(P), or: P ∨ Q, not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), false: False, nequal: a ≠ b ∈ T , int_lower: {...i}
Lemmas referenced : divides_wf, set_subtype_base, nequal_wf, int_subtype_base, int_nzero_wf, istype-int, nat_plus_wf, istype-nat, equal_wf, squash_wf, true_wf, istype-universe, rem_to_div, nat_plus_inc_int_nzero, subtype_rel_self, iff_weakening_equal, div_elim, equal-wf-base, less_than_wf, le_wf, mul_cancel_in_le, mul_cancel_in_lt, add_mono_wrt_eq, subtract_wf, nat_properties, nat_plus_properties, decidable__equal_int, full-omega-unsat, intformand_wf, intformnot_wf, intformeq_wf, itermVar_wf, intformless_wf, itermAdd_wf, itermConstant_wf, intformle_wf, int_formula_prop_and_lemma, int_formula_prop_not_lemma, int_formula_prop_eq_lemma, int_term_value_var_lemma, int_formula_prop_less_lemma, int_term_value_add_lemma, int_term_value_constant_lemma, int_formula_prop_le_lemma, int_formula_prop_wf, itermSubtract_wf, itermMultiply_wf, int_term_value_subtract_lemma, int_term_value_mul_lemma, decidable__le, istype-le, int_nzero_properties, decidable__lt, istype-less_than, rem_sym, itermMinus_wf, int_term_value_minus_lemma, minus-one-mul, mul-minus-1, one-mul, divides_invar_1, rem_2_to_1, minus_functionality_wrt_eq, remainder_wfa, divides_invar_2, rem_3_to_1, divide_wfa, subtract-is-int-iff, multiply-is-int-iff, false_wf
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, lambdaFormation_alt, independent_pairFormation, cut, hypothesis, universeIsType, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, thin, setElimination, rename, hypothesisEquality, equalityIstype, inhabitedIsType, sqequalRule, baseApply, closedConclusion, baseClosed, applyEquality, intEquality, lambdaEquality_alt, natural_numberEquality, independent_isectElimination, sqequalBase, equalitySymmetry, imageElimination, equalityTransitivity, instantiate, universeEquality, imageMemberEquality, because_Cache, productElimination, independent_functionElimination, dependent_functionElimination, hyp_replacement, applyLambdaEquality, multiplyEquality, addEquality, unionElimination, approximateComputation, dependent_pairFormation_alt, int_eqEquality, Error :memTop, voidElimination, dependent_set_memberEquality_alt, minusEquality, pointwiseFunctionality, promote_hyp

Latex:
\mforall{}a:\mBbbZ{}. \mforall{}b:\mBbbZ{}\msupminus{}\msupzero{}. (b | a \mLeftarrow{}{}\mRightarrow{} (a rem b) = 0) Date html generated: 2020_05_19-PM-10_01_00 Last ObjectModification: 2019_12_31-AM-11_15_27 Theory : num_thy_1 Home Index