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. ceige
  55. ceilge
  56. ceim1l
  57. ceilm1lt
  58. ceile
  59. ceille
  60. ceilid
  61. ceilidz
  62. flleceil
  63. fleqceilz
  64. quoremz
  65. quoremnn0
  66. quoremnn0ALT
  67. intfrac2
  68. intfracq
  69. fldiv
  70. fldiv2
  71. fznnfl
  72. uzsup
  73. ioopnfsup
  74. icopnfsup
  75. rpsup
  76. resup
  77. xrsup