### Nuprl Lemma : modulus-is-rem

[a:ℕ]. ∀[n:ℤ-o].  (a mod rem n)

Proof

Definitions occuring in Statement :  modulus: mod n int_nzero: -o nat: uall: [x:A]. B[x] remainder: rem m sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a nat: so_lambda: λ2x.t[x] so_apply: x[s] modulus: mod n has-value: (a)↓ int_nzero: -o nequal: a ≠ b ∈  not: ¬A implies:  Q false: False prop: all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q less_than: a < b less_than': less_than'(a;b) top: Top true: True squash: T decidable: Dec(P) or: P ∨ Q nat_plus: + le: A ≤ B guard: {T} int_lower: {...i} iff: ⇐⇒ Q rev_implies:  Q subtract: m subtype_rel: A ⊆B bfalse: ff exists: x:A. B[x] sq_type: SQType(T) bnot: ¬bb ifthenelse: if then else fi  assert: b gt: i > j
Lemmas referenced :  subtype_base_sq nat_wf set_subtype_base le_wf int_subtype_base value-type-has-value int-value-type equal_wf lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf decidable__lt rem_bounds_1 less_than_transitivity1 less_than_irreflexivity rem_bounds_4 decidable__le false_wf not-le-2 not-equal-2 condition-implies-le minus-zero add-zero minus-add minus-minus add-swap add-commutes add-associates zero-add add_functionality_wrt_le le-add-cancel not-lt-2 eqff_to_assert bool_cases_sqequal bool_subtype_base iff_transitivity assert_wf bnot_wf not_wf iff_weakening_uiff assert_of_bnot not-gt-2 int_nzero_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesis independent_isectElimination sqequalRule intEquality lambdaEquality natural_numberEquality hypothesisEquality callbyvalueReduce remainderEquality setElimination rename because_Cache lambdaFormation independent_functionElimination voidElimination unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination lessCases sqequalAxiom isect_memberEquality independent_pairFormation voidEquality imageMemberEquality baseClosed imageElimination dependent_functionElimination dependent_set_memberEquality minusEquality addEquality applyEquality dependent_pairFormation promote_hyp impliesFunctionality

Latex:
\mforall{}[a:\mBbbN{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (a  mod  n  \msim{}  a  rem  n)

Date html generated: 2017_04_14-AM-07_19_04
Last ObjectModification: 2017_02_27-PM-02_53_16

Theory : arithmetic

Home Index