### Nuprl Lemma : div_floor_wf

[a:ℤ]. ∀[n:ℤ-o].  (a ÷↓ n ∈ ℤ)

Proof

Definitions occuring in Statement :  div_floor: a ÷↓ n int_nzero: -o uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T div_floor: a ÷↓ n int_nzero: -o all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a less_than: a < b less_than': less_than'(a;b) top: Top true: True squash: T not: ¬A false: False prop: has-value: (a)↓ nequal: a ≠ b ∈  guard: {T} bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) bnot: ¬bb ifthenelse: if then else fi  assert: b iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf value-type-has-value int-value-type less_than_transitivity1 le_weakening less_than_irreflexivity equal_wf subtract_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base iff_transitivity assert_wf bnot_wf not_wf iff_weakening_uiff assert_of_bnot int_nzero_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis natural_numberEquality lambdaFormation unionElimination equalityElimination because_Cache productElimination independent_isectElimination lessCases axiomSqEquality isect_memberEquality independent_pairFormation voidElimination voidEquality imageMemberEquality baseClosed imageElimination independent_functionElimination callbyvalueReduce intEquality remainderEquality equalitySymmetry dependent_functionElimination equalityTransitivity divideEquality dependent_pairFormation promote_hyp instantiate cumulativity impliesFunctionality axiomEquality

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (a  \mdiv{}\mdownarrow{}  n  \mmember{}  \mBbbZ{})

Date html generated: 2019_06_20-AM-11_25_38
Last ObjectModification: 2018_08_20-PM-09_28_22

Theory : arithmetic

Home Index