### Nuprl Lemma : rem-sign

`∀[a:ℤ]. ∀[n:ℤ-o].  (((0 ≤ a) `` (0 ≤ (a rem n))) ∧ (0 < a rem n `` 0 < a) ∧ (a rem n < 0 `` a < 0))`

Proof

Definitions occuring in Statement :  int_nzero: `ℤ-o` less_than: `a < b` uall: `∀[x:A]. B[x]` le: `A ≤ B` implies: `P `` Q` and: `P ∧ Q` remainder: `n rem m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` int_nzero: `ℤ-o` decidable: `Dec(P)` or: `P ∨ Q` and: `P ∧ Q` cand: `A c∧ B` implies: `P `` Q` uall: `∀[x:A]. B[x]` nat: `ℕ` prop: `ℙ` nat_plus: `ℕ+` le: `A ≤ B` nequal: `a ≠ b ∈ T ` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` uimplies: `b supposing a` less_than': `less_than'(a;b)` true: `True` subtract: `n - m` subtype_rel: `A ⊆r B` top: `Top` int_lower: `{...i}` rev_uimplies: `rev_uimplies(P;Q)` guard: `{T}` gt: `i > j` ge: `i ≥ j `
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin natural_numberEquality setElimination rename hypothesisEquality hypothesis unionElimination lambdaFormation isectElimination dependent_set_memberEquality productElimination independent_pairFormation voidElimination independent_functionElimination independent_isectElimination addEquality sqequalRule minusEquality applyEquality lambdaEquality isect_memberEquality voidEquality because_Cache remainderEquality intEquality inlFormation inrFormation addLevel orFunctionality isect_memberFormation introduction independent_pairEquality axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (((0  \mleq{}  a)  {}\mRightarrow{}  (0  \mleq{}  (a  rem  n)))  \mwedge{}  (0  <  a  rem  n  {}\mRightarrow{}  0  <  a)  \mwedge{}  (a  rem  n  <  0  {}\mRightarrow{}  a  <  0))

Date html generated: 2016_05_13-PM-03_34_47
Last ObjectModification: 2015_12_26-AM-09_43_57

Theory : arithmetic

Home Index