### Nuprl Lemma : rem_bounds_z

`∀[a:ℤ]. ∀[b:ℤ-o].  |a rem b| < |b|`

Proof

Definitions occuring in Statement :  absval: `|i|` int_nzero: `ℤ-o` less_than: `a < b` uall: `∀[x:A]. B[x]` remainder: `n rem m` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` subtype_rel: `A ⊆r B` nat: `ℕ` uimplies: `b supposing a`
Lemmas referenced :  rem_bounds_absval int_nzero_wf member-less_than absval_wf equal_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis sqequalRule isect_memberEquality isectElimination remainderEquality setElimination rename lambdaFormation independent_functionElimination voidElimination intEquality natural_numberEquality applyEquality because_Cache lambdaEquality independent_isectElimination

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}].    |a  rem  b|  <  |b|

Date html generated: 2016_05_13-PM-03_36_43
Last ObjectModification: 2015_12_26-AM-09_42_17

Theory : arithmetic

Home Index