Nuprl Lemma : mod_bounds

[a:ℤ]. ∀[n:ℕ+].  ((0 ≤ (a mod n)) ∧ mod n < n)


Proof




Definitions occuring in Statement :  modulus: mod n nat_plus: + less_than: a < b uall: [x:A]. B[x] le: A ≤ B and: P ∧ Q natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B nat_plus: + int_nzero: -o so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a prop: all: x:A. B[x] implies:  Q nequal: a ≠ b ∈  not: ¬A false: False guard: {T} and: P ∧ Q squash: T le: A ≤ B true: True iff: ⇐⇒ Q
Lemmas referenced :  nat_plus_wf iff_weakening_equal nat_plus_subtype_nat absval_pos true_wf squash_wf equal_wf less_than_irreflexivity le_weakening less_than_transitivity1 nequal_wf less_than_wf subtype_rel_sets mod_bounds_1
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality sqequalRule intEquality because_Cache lambdaEquality natural_numberEquality independent_isectElimination setElimination rename setEquality lambdaFormation dependent_functionElimination independent_functionElimination voidElimination independent_pairFormation productElimination promote_hyp imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed universeEquality

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    ((0  \mleq{}  (a  mod  n))  \mwedge{}  a  mod  n  <  n)



Date html generated: 2016_05_13-PM-03_37_33
Last ObjectModification: 2016_01_14-PM-06_38_58

Theory : arithmetic


Home Index