Metamath Proof Explorer

Table of Contents - 15.6.5. Dyadic fractions

1. c2s
2. df-2s
3. cexps
4. df-exps
5. cz12s
6. df-z12s
7. 1p1e2s
8. no2times
9. 2nns
10. 2no
11. 2ne0s
12. n0seo
13. zseo
14. twocut
15. nohalf
16. expsval
17. expnnsval
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. pw2divmulsd
32. pw2divscan3d
33. pw2divscan2d
34. pw2divsassd
35. pw2divscan4d
36. pw2gt0divsd
37. pw2ge0divsd
38. pw2divsrecd
39. pw2divsdird
40. pw2divsnegd
41. pw2ltdivmulsd
42. pw2ltmuldivs2d
43. pw2ltsdiv1d
44. avglts1d
45. avglts2d
46. pw2divs0d
47. pw2divsidd
48. pw2ltdivmuls2d
49. halfcut
50. addhalfcut
51. pw2cut
52. pw2cutp1
53. pw2cut2
54. bdaypw2n0bndlem
55. bdaypw2n0bnd
56. bdaypw2bnd
57. bdayfinbndcbv
58. bdayfinbndlem1
59. bdayfinbndlem2
60. bdayfinbnd
61. z12bdaylem1
62. z12bdaylem2
63. elz12s
64. elz12si
65. z12sex
66. zz12s
67. z12no
68. z12addscl
69. z12negscl
70. z12subscl
71. z12shalf
72. z12negsclb
73. z12zsodd
74. z12sge0
75. z12bdaylem
76. z12bday
77. bdayfinlem
78. bdayfin
79. dfz12s2