### Nuprl Lemma : posint_div_dec

`∀a,b:|<ℤ+,*>|.  Dec(a | b)`

Proof

Definitions occuring in Statement :  posint_mul_mon: `<ℤ+,*>` mdivides: `b | a` decidable: `Dec(P)` all: `∀x:A. B[x]` grp_car: `|g|`
Definitions unfolded in proof :  posint_mul_mon: `<ℤ+,*>` mdivides: `b | a` grp_car: `|g|` pi1: `fst(t)` grp_op: `*` pi2: `snd(t)` infix_ap: `x f y` all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` nat_plus: `ℕ+` subtype_rel: `A ⊆r B` decidable: `Dec(P)` or: `P ∨ Q` exists: `∃x:A. B[x]` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` not: `¬A` implies: `P `` Q` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` and: `P ∧ Q` prop: `ℙ` le: `A ≤ B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` guard: `{T}` less_than: `a < b` squash: `↓T`
Lemmas referenced :  nat_plus_wf decidable__equal_int remainder_wfa nat_plus_inc_int_nzero div_rem_sum div_bounds_1 nat_plus_subtype_nat nat_plus_properties divide_wfa full-omega-unsat intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_wf int_subtype_base nequal_wf intformnot_wf itermMultiply_wf itermAdd_wf int_formula_prop_not_lemma int_term_value_mul_lemma int_term_value_add_lemma decidable__lt istype-less_than set_subtype_base less_than_wf subtype_base_sq intformle_wf int_formula_prop_le_lemma rem-exact
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule lambdaFormation_alt inhabitedIsType hypothesisEquality universeIsType cut introduction extract_by_obid hypothesis sqequalHypSubstitution dependent_functionElimination thin isectElimination setElimination rename applyEquality natural_numberEquality unionElimination inlFormation_alt dependent_pairFormation_alt because_Cache multiplyEquality dependent_set_memberEquality_alt independent_isectElimination approximateComputation independent_functionElimination lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation equalityIstype baseClosed sqequalBase equalitySymmetry intEquality equalityTransitivity productElimination functionIsType productIsType baseApply closedConclusion instantiate cumulativity imageElimination imageMemberEquality equalityIsType4 inrFormation_alt

Latex:
\mforall{}a,b:|<\mBbbZ{}\msupplus{},*>|.    Dec(a  |  b)

Date html generated: 2019_10_16-PM-01_06_11
Last ObjectModification: 2019_06_20-PM-06_44_22

Theory : factor_1

Home Index