Metamath Proof Explorer


Table of Contents - 20.43.22.10. Digits

Generalization of df-bits. In contrast to , are defined for integers only. The equivalence of both definitions for integers is shown in dig2bits: if and are nonnegative integers, then .

  1. cdig
  2. df-dig
  3. digfval
  4. digval
  5. digvalnn0
  6. nn0digval
  7. dignn0fr
  8. dignn0ldlem
  9. dignnld
  10. dig2nn0ld
  11. dig2nn1st
  12. dig0
  13. digexp
  14. dig1
  15. 0dig1
  16. 0dig2pr01
  17. dig2nn0
  18. 0dig2nn0e
  19. 0dig2nn0o
  20. dig2bits