Metamath Proof Explorer


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).

  1. Definitions and basic properties
    1. ceven
    2. codd
    3. df-even
    4. df-odd
    5. iseven
    6. isodd
    7. evenz
    8. oddz
    9. evendiv2z
    10. oddp1div2z
    11. oddm1div2z
    12. isodd2
    13. dfodd2
    14. dfodd6
    15. dfeven4
    16. evenm1odd
    17. evenp1odd
    18. oddp1eveni
    19. oddm1eveni
    20. evennodd
    21. oddneven
    22. enege
    23. onego
    24. m1expevenALTV
    25. m1expoddALTV
  2. Alternate definitions using the "divides" relation
    1. dfeven2
    2. dfodd3
    3. iseven2
    4. isodd3
    5. 2dvdseven
    6. m2even
    7. 2ndvdsodd
    8. 2dvdsoddp1
    9. 2dvdsoddm1
  3. Alternate definitions using the "modulo" operation
    1. dfeven3
    2. dfodd4
    3. dfodd5
    4. zefldiv2ALTV
    5. zofldiv2ALTV
    6. oddflALTV
  4. Alternate definitions using the "gcd" operation
    1. iseven5
    2. isodd7
    3. dfeven5
    4. dfodd7
    5. gcd2odd1
  5. Theorems of part 5 revised
    1. zneoALTV
    2. zeoALTV
    3. zeo2ALTV
    4. nneoALTV
    5. nneoiALTV
  6. Theorems of part 6 revised
    1. odd2np1ALTV
    2. oddm1evenALTV
    3. oddp1evenALTV
    4. oexpnegALTV
    5. oexpnegnz
    6. bits0ALTV
    7. bits0eALTV
    8. bits0oALTV
    9. divgcdoddALTV
    10. opoeALTV
    11. opeoALTV
    12. omoeALTV
    13. omeoALTV
    14. oddprmALTV
  7. Theorems of AV's mathbox revised
    1. 0evenALTV
    2. 0noddALTV
    3. 1oddALTV
    4. 1nevenALTV
    5. 2evenALTV
    6. 2noddALTV
    7. nn0o1gt2ALTV
    8. nnoALTV
    9. nn0oALTV
    10. nn0e
    11. nneven
    12. nn0onn0exALTV
    13. nn0enn0exALTV
    14. nnennexALTV
    15. nnpw2evenALTV
  8. Additional theorems
    1. epoo
    2. emoo
    3. epee
    4. emee
    5. evensumeven
    6. 3odd
    7. 4even
    8. 5odd
    9. 6even
    10. 7odd
    11. 8even
    12. evenprm2
    13. oddprmne2
    14. oddprmuzge3
    15. evenltle
    16. odd2prm2
    17. even3prm2
    18. mogoldbblem
  9. Perfect Number Theorem (revised)
    1. perfectALTVlem1
    2. perfectALTVlem2
    3. perfectALTV