Divp-by-casting
Generalized version of casting out nines
In this book we prove the general theorem that the divisibility of
n by d can be determined by recursively summing the base-b
digits of n and then checking that the final sum is divisible by d,
provided n, d and b are naturals, d and b are
greater than 1, and b is equivalent to 1 mod d. We then prove
corollaries that show ``casting out 9s'' and ``casting out 3s'' work
correctly when decimal (base b = 10) digits are extracted and summed.
We also show that ``casting out 7s'' works when octal (base b = 8)
digits are extracted and summed. Furthermore, we prove that casting out 7s
can be computed using the logical operations logand and ash
instead of mod and floor.
The proof of the general theorem requires non-linear arithmetic since
d and b are variables, whereas in the corollaries b and d
are constants, e.g., 10 and 3 or 8 and 7. So use is made of the powerful
arithmetic book arithmetic-5/top. This book provides rules for
manipulating many arithmetic primitives, including mod and floor
and is able to handle many non-linear arithmetic problems heuristically.
However, (a) arithmetic-5/top does not rewrite mod and floor
expressions as we wanted them rewritten for this proof, and (b)
arithmetic-5/top sometimes goes into an infinite loop in its attempt to
reason about multiplication. So perhaps the most important lesson to be
gained from this book is an illustration of one way to manage such problems
while still using arithmetic-5/top on the problems it can solve. For
that reason, we've taken special care to describe how the proof script here
was created. For further details, read the extensive comments in the
divp-by-casting book.
