### Nuprl Lemma : absval_div_nat

`∀[n:ℕ+]. ∀[i:ℤ].  (|i| ÷ n ~ |i ÷ n|)`

Proof

Definitions occuring in Statement :  absval: `|i|` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` divide: `n ÷ m` int: `ℤ` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` sq_type: `SQType(T)` implies: `P `` Q` guard: `{T}` nat: `ℕ` prop: `ℙ` squash: `↓T` nat_plus: `ℕ+` nequal: `a ≠ b ∈ T ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` and: `P ∧ Q` subtype_rel: `A ⊆r B` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` int_lower: `{...i}` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` less_than: `a < b` less_than': `less_than'(a;b)` bfalse: `ff` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b`
Lemmas referenced :  subtype_base_sq int_subtype_base decidable__le nat_plus_wf div_bounds_1 le_wf equal_wf squash_wf true_wf absval_pos nat_plus_properties full-omega-unsat intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_wf equal-wf-base divide_wf subtype_rel_self iff_weakening_equal div_bounds_2 intformnot_wf intformle_wf int_formula_prop_not_lemma int_formula_prop_le_lemma absval_unfold2 lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot minus_functionality_wrt_eq div_2_to_1 minus_minus_cancel
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination cumulativity intEquality independent_isectElimination hypothesis dependent_functionElimination natural_numberEquality hypothesisEquality unionElimination equalityTransitivity equalitySymmetry independent_functionElimination sqequalAxiom sqequalRule isect_memberEquality because_Cache dependent_set_memberEquality applyEquality lambdaEquality imageElimination universeEquality divideEquality setElimination rename lambdaFormation approximateComputation dependent_pairFormation int_eqEquality voidElimination voidEquality independent_pairFormation baseClosed imageMemberEquality productElimination minusEquality equalityElimination lessCases promote_hyp

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[i:\mBbbZ{}].    (|i|  \mdiv{}  n  \msim{}  |i  \mdiv{}  n|)

Date html generated: 2018_05_21-PM-00_30_20
Last ObjectModification: 2018_05_15-PM-05_47_32

Theory : int_2

Home Index