NUM_MOD_CONV : term -> thm
Proves what the remainder on dividing one natural number numeral by another is.
If n and m are numerals (e.g. 0, 1, 2, 3,...), then
NUM_MOD_CONV `n MOD m` returns the theorem:
where s is the numeral that denotes the remainder on dividing
the number denoted by n by the one denoted by m.
- FAILURE CONDITIONS
NUM_MOD_CONV tm fails if tm is not of the form `n MOD m`, where n and
m are numerals, or if the second numeral m is zero.
# NUM_MOD_CONV `1089 MOD 9`;;
val it : thm = |- 1089 MOD 9 = 0
# NUM_MOD_CONV `1234 MOD 3`;;
val it : thm = |- 1234 MOD 3 = 1
# NUM_MOD_CONV `11 MOD 0`;;
Exception: Failure "NUM_MOD_CONV".
For definiteness, remainders with zero denominator are in fact designed to be
zero. However, it is perhaps bad style to rely on this fact, so the conversion
just fails in this case.
- SEE ALSO
NUM_ADD_CONV, NUM_DIV_CONV, NUM_EQ_CONV, NUM_EVEN_CONV,
NUM_EXP_CONV, NUM_FACT_CONV, NUM_GE_CONV, NUM_GT_CONV, NUM_LE_CONV,
NUM_LT_CONV, NUM_MAX_CONV, NUM_MIN_CONV, NUM_MULT_CONV, NUM_ODD_CONV,
NUM_PRE_CONV, NUM_REDUCE_CONV, NUM_RED_CONV, NUM_REL_CONV, NUM_SUB_CONV,