### Nuprl Lemma : rem_bounds_absval_le

`∀b:ℤ-o. ∀a:ℤ.  (|a rem b| ≤ |b|)`

Proof

Definitions occuring in Statement :  absval: `|i|` int_nzero: `ℤ-o` le: `A ≤ B` all: `∀x:A. B[x]` remainder: `n rem m` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` guard: `{T}` uall: `∀[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 le_weakening2 absval_wf equal_wf nat_wf int_nzero_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination remainderEquality setElimination rename independent_functionElimination voidElimination intEquality natural_numberEquality applyEquality because_Cache sqequalRule lambdaEquality independent_isectElimination

Latex:
\mforall{}b:\mBbbZ{}\msupminus{}\msupzero{}.  \mforall{}a:\mBbbZ{}.    (|a  rem  b|  \mleq{}  |b|)

Date html generated: 2016_05_13-PM-03_34_59
Last ObjectModification: 2015_12_26-AM-09_43_21

Theory : arithmetic

Home Index