Table of Contents - 20.43.13. Even and odd numbers
Even and odd numbers can be characterized in many different ways. In the
following, the definition of even and odd numbers is based on the fact that
dividing an even number (resp. an odd number increased by 1) by 2 is an
integer, see df-even and df-odd. Alternate definitions resp.
characterizations are provided in dfeven2, dfeven3, dfeven4 and in
dfodd2, dfodd3, dfodd4, dfodd5, dfodd6. Each characterization
can be useful (and used) in an appropriate context, e.g. dfodd6 in
opoeALTV and dfodd3 in oddprmALTV. Having a fixed definition for even
and odd numbers, and alternate characterizations as theorems, advanced
theorems about even and/or odd numbers can be expressed more explicitly, and
the appropriate characterization can be chosen for their proof, which may
become clearer and sometimes also shorter (see, for example, divgcdoddALTV and divgcdodd).