Metamath Proof Explorer

Table of Contents - 15.6.5. Dyadic fractions

  1. c2s
  2. df-2s
  3. cexps
  4. df-exps
  5. czs12
  6. df-zs12
  7. 1p1e2s
  8. no2times
  9. 2nns
  10. 2sno
  11. 2ne0s
  12. n0seo
  13. zseo
  14. twocut
  15. nohalf
  16. expsval
  17. expsnnval
  18. exps0
  19. exps1
  20. expsp1
  21. expscllem
  22. expscl
  23. n0expscl
  24. nnexpscl
  25. zexpscl
  26. expadds
  27. expsne0
  28. expsgt0
  29. pw2recs
  30. pw2divscld
  31. pw2divsmuld
  32. pw2divscan3d
  33. pw2divscan2d
  34. pw2divsassd
  35. pw2divscan4d
  36. pw2gt0divsd
  37. pw2ge0divsd
  38. pw2divsrecd
  39. pw2divsdird
  40. pw2divsnegd
  41. pw2sltdivmuld
  42. pw2sltmuldiv2d
  43. avgslt1d
  44. avgslt2d
  45. halfcut
  46. addhalfcut
  47. pw2cut
  48. pw2cutp1
  49. elzs12
  50. zs12ex
  51. zzs12
  52. zs12no
  53. zs12addscl
  54. zs12negscl
  55. zs12subscl
  56. zs12half
  57. zs12negsclb
  58. zs12zodd
  59. zs12ge0
  60. zs12bday