Metamath Proof Explorer


Table of Contents - 5.6. Elementary integer functions

  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
  2. The modulo (remainder) operation
    1. cmo
    2. df-mod
    3. modval
    4. modvalr
    5. modcl
    6. flpmodeq
    7. modcld
    8. mod0
    9. mulmod0
    10. negmod0
    11. modge0
    12. modlt
    13. modelico
    14. moddiffl
    15. moddifz
    16. modfrac
    17. flmod
    18. intfrac
    19. zmod10
    20. zmod1congr
    21. modmulnn
    22. modvalp1
    23. zmodcl
    24. zmodcld
    25. zmodfz
    26. zmodfzo
    27. zmodfzp1
    28. modid
    29. modid0
    30. modid2
    31. zmodid2
    32. zmodidfzo
    33. zmodidfzoimp
    34. 0mod
    35. 1mod
    36. modabs
    37. modabs2
    38. modcyc
    39. modcyc2
    40. modadd1
    41. modaddabs
    42. modaddmod
    43. muladdmodid
    44. mulp1mod1
    45. modmuladd
    46. modmuladdim
    47. modmuladdnn0
    48. negmod
    49. m1modnnsub1
    50. m1modge3gt1
    51. addmodid
    52. addmodidr
    53. modadd2mod
    54. modm1p1mod0
    55. modltm1p1mod
    56. modmul1
    57. modmul12d
    58. modnegd
    59. modadd12d
    60. modsub12d
    61. modsubmod
    62. modsubmodmod
    63. 2txmodxeq0
    64. 2submod
    65. modifeq2int
    66. modaddmodup
    67. modaddmodlo
    68. modmulmod
    69. modmulmodr
    70. modaddmulmod
    71. moddi
    72. modsubdir
    73. modeqmodmin
    74. modirr
    75. modfzo0difsn
    76. modsumfzodifsn
    77. modlteq
    78. addmodlteq
  3. Miscellaneous theorems about integers
    1. om2uz0i
    2. om2uzsuci
    3. om2uzuzi
    4. om2uzlti
    5. om2uzlt2i
    6. om2uzrani
    7. om2uzf1oi
    8. om2uzisoi
    9. om2uzoi
    10. om2uzrdg
    11. uzrdglem
    12. uzrdgfni
    13. uzrdg0i
    14. uzrdgsuci
    15. ltweuz
    16. ltwenn
    17. ltwefz
    18. uzenom
    19. uzinf
    20. nnnfi
    21. uzrdgxfr
    22. fzennn
    23. fzen2
    24. cardfz
    25. hashgf1o
    26. fzfi
    27. fzfid
    28. fzofi
    29. fsequb
    30. fsequb2
    31. fseqsupcl
    32. fseqsupubi
    33. nn0ennn
    34. nnenom
    35. nnct
    36. uzindi
    37. axdc4uzlem
    38. axdc4uz
    39. ssnn0fi
    40. rabssnn0fi
  4. Strong induction over upper sets of integers
    1. uzsinds
    2. nnsinds
    3. nn0sinds
  5. Finitely supported functions over the nonnegative integers
    1. fsuppmapnn0fiublem
    2. fsuppmapnn0fiub
    3. fsuppmapnn0fiubex
    4. fsuppmapnn0fiub0
    5. suppssfz
    6. fsuppmapnn0ub
    7. fsuppmapnn0fz
    8. mptnn0fsupp
    9. mptnn0fsuppd
    10. mptnn0fsuppr
    11. f13idfv
  6. The infinite sequence builder "seq" - extension
    1. cseq
    2. df-seq
    3. seqex
    4. seqeq1
    5. seqeq2
    6. seqeq3
    7. seqeq1d
    8. seqeq2d
    9. seqeq3d
    10. seqeq123d
    11. nfseq
    12. seqval
    13. seqfn
    14. seq1
    15. seq1i
    16. seqp1
    17. seqexw
    18. seqp1d
    19. seqp1iOLD
    20. seqm1
    21. seqcl2
    22. seqf2
    23. seqcl
    24. seqf
    25. seqfveq2
    26. seqfeq2
    27. seqfveq
    28. seqfeq
    29. seqshft2
    30. seqres
    31. serf
    32. serfre
    33. monoord
    34. monoord2
    35. sermono
    36. seqsplit
    37. seq1p
    38. seqcaopr3
    39. seqcaopr2
    40. seqcaopr
    41. seqf1olem2a
    42. seqf1olem1
    43. seqf1olem2
    44. seqf1o
    45. seradd
    46. sersub
    47. seqid3
    48. seqid
    49. seqid2
    50. seqhomo
    51. seqz
    52. seqfeq4
    53. seqfeq3
    54. seqdistr
    55. ser0
    56. ser0f
    57. serge0
    58. serle
    59. ser1const
    60. seqof
    61. seqof2
  7. Integer powers
    1. cexp
    2. df-exp
    3. expval
    4. expnnval
    5. exp0
    6. 0exp0e1
    7. exp1
    8. expp1
    9. expneg
    10. expneg2
    11. expn1
    12. expcllem
    13. expcl2lem
    14. nnexpcl
    15. nn0expcl
    16. zexpcl
    17. qexpcl
    18. reexpcl
    19. expcl
    20. rpexpcl
    21. reexpclz
    22. qexpclz
    23. m1expcl2
    24. m1expcl
    25. expclzlem
    26. expclz
    27. nn0expcli
    28. nn0sqcl
    29. expm1t
    30. 1exp
    31. expeq0
    32. expne0
    33. expne0i
    34. expgt0
    35. expnegz
    36. 0exp
    37. expge0
    38. expge1
    39. expgt1
    40. mulexp
    41. mulexpz
    42. exprec
    43. expadd
    44. expaddzlem
    45. expaddz
    46. expmul
    47. expmulz
    48. m1expeven
    49. expsub
    50. expp1z
    51. expm1
    52. expdiv
    53. sqval
    54. sqneg
    55. sqsubswap
    56. sqcl
    57. sqmul
    58. sqeq0
    59. sqdiv
    60. sqdivid
    61. sqne0
    62. resqcl
    63. sqgt0
    64. sqn0rp
    65. nnsqcl
    66. zsqcl
    67. qsqcl
    68. sq11
    69. nn0sq11
    70. lt2sq
    71. le2sq
    72. le2sq2
    73. sqge0
    74. zsqcl2
    75. 0expd
    76. exp0d
    77. exp1d
    78. expeq0d
    79. sqvald
    80. sqcld
    81. sqeq0d
    82. expcld
    83. expp1d
    84. expaddd
    85. expmuld
    86. sqrecd
    87. expclzd
    88. expne0d
    89. expnegd
    90. exprecd
    91. expp1zd
    92. expm1d
    93. expsubd
    94. sqmuld
    95. sqdivd
    96. expdivd
    97. mulexpd
    98. znsqcld
    99. reexpcld
    100. expge0d
    101. expge1d
    102. ltexp2a
    103. expmordi
    104. rpexpmord
    105. expcan
    106. ltexp2
    107. leexp2
    108. leexp2a
    109. ltexp2r
    110. leexp2r
    111. leexp1a
    112. exple1
    113. expubnd
    114. sumsqeq0
    115. sqvali
    116. sqcli
    117. sqeq0i
    118. sqrecii
    119. sqmuli
    120. sqdivi
    121. resqcli
    122. sqgt0i
    123. sqge0i
    124. lt2sqi
    125. le2sqi
    126. sq11i
    127. sq0
    128. sq0i
    129. sq0id
    130. sq1
    131. neg1sqe1
    132. sq2
    133. sq3
    134. sq4e2t8
    135. cu2
    136. irec
    137. i2
    138. i3
    139. i4
    140. nnlesq
    141. iexpcyc
    142. expnass
    143. sqlecan
    144. subsq
    145. subsq2
    146. binom2i
    147. subsqi
    148. sqeqori
    149. subsq0i
    150. sqeqor
    151. binom2
    152. binom21
    153. binom2sub
    154. binom2sub1
    155. binom2subi
    156. mulbinom2
    157. binom3
    158. sq01
    159. zesq
    160. nnesq
    161. crreczi
    162. bernneq
    163. bernneq2
    164. bernneq3
    165. expnbnd
    166. expnlbnd
    167. expnlbnd2
    168. expmulnbnd
    169. digit2
    170. digit1
    171. modexp
    172. discr1
    173. discr
    174. expnngt1
    175. expnngt1b
    176. sqoddm1div8
    177. nnsqcld
    178. nnexpcld
    179. nn0expcld
    180. rpexpcld
    181. ltexp2rd
    182. reexpclzd
    183. resqcld
    184. sqge0d
    185. sqgt0d
    186. ltexp2d
    187. leexp2d
    188. expcand
    189. leexp2ad
    190. leexp2rd
    191. lt2sqd
    192. le2sqd
    193. sq11d
    194. mulsubdivbinom2
    195. muldivbinom2
    196. sq10
    197. sq10e99m1
    198. 3dec
  8. Ordered pair theorem for nonnegative integers
    1. nn0le2msqi
    2. nn0opthlem1
    3. nn0opthlem2
    4. nn0opthi
    5. nn0opth2i
    6. nn0opth2
  9. Factorial function
    1. cfa
    2. df-fac
    3. facnn
    4. fac0
    5. fac1
    6. facp1
    7. fac2
    8. fac3
    9. fac4
    10. facnn2
    11. faccl
    12. faccld
    13. facmapnn
    14. facne0
    15. facdiv
    16. facndiv
    17. facwordi
    18. faclbnd
    19. faclbnd2
    20. faclbnd3
    21. faclbnd4lem1
    22. faclbnd4lem2
    23. faclbnd4lem3
    24. faclbnd4lem4
    25. faclbnd4
    26. faclbnd5
    27. faclbnd6
    28. facubnd
    29. facavg
  10. The binomial coefficient operation
    1. cbc
    2. df-bc
    3. bcval
    4. bcval2
    5. bcval3
    6. bcval4
    7. bcrpcl
    8. bccmpl
    9. bcn0
    10. bc0k
    11. bcnn
    12. bcn1
    13. bcnp1n
    14. bcm1k
    15. bcp1n
    16. bcp1nk
    17. bcval5
    18. bcn2
    19. bcp1m1
    20. bcpasc
    21. bccl
    22. bccl2
    23. bcn2m1
    24. bcn2p1
    25. permnn
    26. bcnm1
    27. 4bc3eq4
    28. 4bc2eq6
  11. The ` # ` (set size) function
    1. chash
    2. df-hash
    3. hashkf
    4. hashgval
    5. hashginv
    6. hashinf
    7. hashbnd
    8. hashfxnn0
    9. hashf
    10. hashxnn0
    11. hashresfn
    12. dmhashres
    13. hashnn0pnf
    14. hashnnn0genn0
    15. hashnemnf
    16. hashv01gt1
    17. hashfz1
    18. hashen
    19. hasheni
    20. hasheqf1o
    21. fiinfnf1o
    22. focdmex
    23. hasheqf1oi
    24. hashf1rn
    25. hasheqf1od
    26. fz1eqb
    27. hashcard
    28. hashcl
    29. hashxrcl
    30. hashclb
    31. nfile
    32. hashvnfin
    33. hashnfinnn0
    34. isfinite4
    35. hasheq0
    36. hashneq0
    37. hashgt0n0
    38. hashnncl
    39. hash0
    40. hashelne0d
    41. hashsng
    42. hashen1
    43. hash1elsn
    44. hashrabrsn
    45. hashrabsn01
    46. hashrabsn1
    47. hashfn
    48. fseq1hash
    49. hashgadd
    50. hashgval2
    51. hashdom
    52. hashdomi
    53. hashsdom
    54. hashun
    55. hashun2
    56. hashun3
    57. hashinfxadd
    58. hashunx
    59. hashge0
    60. hashgt0
    61. hashge1
    62. 1elfz0hash
    63. hashnn0n0nn
    64. hashunsng
    65. hashunsngx
    66. hashunsnggt
    67. hashprg
    68. elprchashprn2
    69. hashprb
    70. hashprdifel
    71. prhash2ex
    72. hashle00
    73. hashgt0elex
    74. hashgt0elexb
    75. hashp1i
    76. hash1
    77. hash2
    78. hash3
    79. hash4
    80. pr0hash2ex
    81. hashss
    82. prsshashgt1
    83. hashin
    84. hashssdif
    85. hashdif
    86. hashdifsn
    87. hashdifpr
    88. hashsn01
    89. hashsnle1
    90. hashsnlei
    91. hash1snb
    92. euhash1
    93. hash1n0
    94. hashgt12el
    95. hashgt12el2
    96. hashgt23el
    97. hashunlei
    98. hashsslei
    99. hashfz
    100. fzsdom2
    101. hashfzo
    102. hashfzo0
    103. hashfzp1
    104. hashfz0
    105. hashxplem
    106. hashxp
    107. hashmap
    108. hashpw
    109. hashfun
    110. hashres
    111. hashreshashfun
    112. hashimarn
    113. hashimarni
    114. resunimafz0
    115. fnfz0hash
    116. ffz0hash
    117. fnfz0hashnn0
    118. ffzo0hash
    119. fnfzo0hash
    120. fnfzo0hashnn0
    121. hashbclem
    122. hashbc
    123. hashfacen
    124. hashf1lem1
    125. hashf1lem2
    126. hashf1
    127. hashfac
    128. leiso
    129. leisorel
    130. fz1isolem
    131. fz1iso
    132. ishashinf
    133. seqcoll
    134. seqcoll2
    135. phphashd
    136. phphashrd
    137. Proper unordered pairs and triples (sets of size 2 and 3)
    138. Functions with a domain containing at least two different elements
    139. Finite induction on the size of the first component of a binary relation