Nuprl Lemma : rem_bounds_1

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


Proof




Definitions occuring in Statement :  nat_plus: + nat: less_than: a < b uall: [x:A]. B[x] le: A ≤ B and: P ∧ Q remainder: rem m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q le: A ≤ B not: ¬A implies:  Q false: False nat: nat_plus: + nequal: a ≠ b ∈  guard: {T} uimplies: supposing a all: x:A. B[x] prop: ge: i ≥  sq_stable: SqStable(P) squash: T gt: i > j
Lemmas referenced :  decidable__le le_wf sq_stable_from_decidable nat_wf nat_plus_wf member-less_than equal_wf less_than_irreflexivity le_weakening less_than_transitivity1 less_than'_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality because_Cache lemma_by_obid isectElimination remainderEquality setElimination rename hypothesis lambdaFormation natural_numberEquality independent_isectElimination independent_functionElimination voidElimination intEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality remainderBounds1 imageMemberEquality baseClosed imageElimination

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



Date html generated: 2016_05_13-PM-03_33_20
Last ObjectModification: 2016_01_14-PM-06_40_39

Theory : arithmetic


Home Index