### 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: `λ2x.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