Nuprl Definition : rem_nrel
Rem(a;n;r) == ∃q:ℕ. (Div(a;n;q) ∧ (((q * n) + r) = a ∈ ℤ))
Definitions occuring in Statement :
div_nrel: Div(a;n;q),
nat: ℕ,
exists: ∃x:A. B[x],
and: P ∧ Q,
multiply: n * m,
add: n + m,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
nat: ℕ,
and: P ∧ Q,
div_nrel: Div(a;n;q),
equal: s = t ∈ T,
int: ℤ,
add: n + m,
multiply: n * m
FDL editor aliases :
rem_nrel
Latex:
Rem(a;n;r) == \mexists{}q:\mBbbN{}. (Div(a;n;q) \mwedge{} (((q * n) + r) = a))
Date html generated:
2016_05_14-AM-07_24_57
Last ObjectModification:
2015_09_22-PM-05_46_19
Theory : int_2
Home
Index