Metamath Proof Explorer

Table of Contents - 5.6.1. The floor and ceiling functions

1. cfl
2. cceil
3. df-fl
4. df-ceil
5. flval
6. flcl
7. reflcl
8. fllelt
9. flcld
10. flle
11. flltp1
12. fllep1
13. fraclt1
14. fracle1
15. fracge0
16. flge
17. fllt
18. flflp1
19. flid
20. flidm
21. flidz
22. flltnz
23. flwordi
24. flword2
25. flval2
26. flval3
27. flbi
28. flbi2
29. adddivflid
30. ico01fl0
31. flge0nn0
32. flge1nn
33. fldivnn0
34. refldivcl
35. divfl0
36. fladdz
37. flzadd
38. flmulnn0
39. btwnzge0
40. 2tnp1ge0ge0
41. flhalf
42. fldivle
43. fldivnn0le
44. flltdivnn0lt
45. ltdifltdiv
46. fldiv4p1lem1div2
47. fldiv4lem1div2uz2
48. fldiv4lem1div2
49. ceilval
50. dfceil2
51. ceilval2
52. ceicl
53. ceilcl
54. ceilcld
55. ceige
56. ceilge
57. ceilged
58. ceim1l
59. ceilm1lt
60. ceile
61. ceille
62. ceilid
63. ceilidz
64. flleceil
65. fleqceilz
66. quoremz
67. quoremnn0
68. quoremnn0ALT
69. intfrac2
70. intfracq
71. fldiv
72. fldiv2
73. fznnfl
74. uzsup
75. ioopnfsup
76. icopnfsup
77. rpsup
78. resup
79. xrsup