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. 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
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. modaddb
   42. modaddid
   43. modaddabs
   44. modaddmod
   45. muladdmodid
   46. mulp1mod1
   47. muladdmod
   48. modmuladd
   49. modmuladdim
   50. modmuladdnn0
   51. negmod
   52. m1modnnsub1
   53. m1modge3gt1
   54. addmodid
   55. addmodidr
   56. modadd2mod
   57. modm1p1mod0
   58. modltm1p1mod
   59. modmul1
   60. modmul12d
   61. modnegd
   62. modadd12d
   63. modsub12d
   64. modsubmod
   65. modsubmodmod
   66. 2txmodxeq0
   67. 2submod
   68. modifeq2int
   69. modaddmodup
   70. modaddmodlo
   71. modmulmod
   72. modmulmodr
   73. modaddmulmod
   74. moddi
   75. modsubdir
   76. modeqmodmin
   77. modirr
   78. modfzo0difsn
   79. modsumfzodifsn
   80. modlteq
   81. 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. seqm1
   20. seqcl2
   21. seqf2
   22. seqcl
   23. seqf
   24. seqfveq2
   25. seqfeq2
   26. seqfveq
   27. seqfeq
   28. seqshft2
   29. seqres
   30. serf
   31. serfre
   32. monoord
   33. monoord2
   34. sermono
   35. seqsplit
   36. seq1p
   37. seqcaopr3
   38. seqcaopr2
   39. seqcaopr
   40. seqf1olem2a
   41. seqf1olem1
   42. seqf1olem2
   43. seqf1o
   44. seradd
   45. sersub
   46. seqid3
   47. seqid
   48. seqid2
   49. seqhomo
   50. seqz
   51. seqfeq4
   52. seqfeq3
   53. seqdistr
   54. ser0
   55. ser0f
   56. serge0
   57. serle
   58. ser1const
   59. seqof
   60. 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. qexpclz
   22. reexpclz
   23. expclzlem
   24. expclz
   25. m1expcl2
   26. m1expcl
   27. zexpcld
   28. nn0expcli
   29. nn0sqcl
   30. expm1t
   31. 1exp
   32. expeq0
   33. expne0
   34. expne0i
   35. expgt0
   36. expnegz
   37. 0exp
   38. expge0
   39. expge1
   40. expgt1
   41. mulexp
   42. mulexpz
   43. exprec
   44. expadd
   45. expaddzlem
   46. expaddz
   47. expmul
   48. expmulz
   49. m1expeven
   50. expsub
   51. expp1z
   52. expm1
   53. expdiv
   54. sqval
   55. sqneg
   56. sqnegd
   57. sqsubswap
   58. sqcl
   59. sqmul
   60. sqeq0
   61. sqdiv
   62. sqdivid
   63. sqne0
   64. resqcl
   65. resqcld
   66. sqgt0
   67. sqn0rp
   68. nnsqcl
   69. zsqcl
   70. qsqcl
   71. sq11
   72. nn0sq11
   73. lt2sq
   74. le2sq
   75. le2sq2
   76. sqge0
   77. sqge0d
   78. zsqcl2
   79. 0expd
   80. exp0d
   81. exp1d
   82. expeq0d
   83. sqvald
   84. sqcld
   85. sqeq0d
   86. expcld
   87. expp1d
   88. expaddd
   89. expmuld
   90. sqrecd
   91. expclzd
   92. expne0d
   93. expnegd
   94. exprecd
   95. expp1zd
   96. expm1d
   97. expsubd
   98. sqmuld
   99. sqdivd
   100. expdivd
   101. mulexpd
   102. znsqcld
   103. reexpcld
   104. expge0d
   105. expge1d
   106. ltexp2a
   107. expmordi
   108. rpexpmord
   109. expcan
   110. ltexp2
   111. leexp2
   112. leexp2a
   113. ltexp2r
   114. leexp2r
   115. leexp1a
   116. leexp1ad
   117. exple1
   118. expubnd
   119. sumsqeq0
   120. sqvali
   121. sqcli
   122. sqeq0i
   123. sqrecii
   124. sqmuli
   125. sqdivi
   126. resqcli
   127. sqgt0i
   128. sqge0i
   129. lt2sqi
   130. le2sqi
   131. sq11i
   132. sq0
   133. sq0i
   134. sq0id
   135. sq1
   136. neg1sqe1
   137. sq2
   138. sq3
   139. sq4e2t8
   140. cu2
   141. irec
   142. i2
   143. i3
   144. i4
   145. nnlesq
   146. zzlesq
   147. iexpcyc
   148. expnass
   149. sqlecan
   150. subsq
   151. subsq2
   152. binom2i
   153. subsqi
   154. sqeqori
   155. subsq0i
   156. sqeqor
   157. binom2
   158. binom2d
   159. binom21
   160. binom2sub
   161. binom2sub1
   162. binom2subi
   163. mulbinom2
   164. binom3
   165. sq01
   166. zesq
   167. nnesq
   168. crreczi
   169. bernneq
   170. bernneq2
   171. bernneq3
   172. expnbnd
   173. expnlbnd
   174. expnlbnd2
   175. expmulnbnd
   176. digit2
   177. digit1
   178. modexp
   179. discr1
   180. discr
   181. expnngt1
   182. expnngt1b
   183. sqoddm1div8
   184. nnsqcld
   185. nnexpcld
   186. nn0expcld
   187. rpexpcld
   188. ltexp2rd
   189. reexpclzd
   190. sqgt0d
   191. ltexp2d
   192. leexp2d
   193. expcand
   194. leexp2ad
   195. leexp2rd
   196. lt2sqd
   197. le2sqd
   198. sq11d
   199. ltexp1d
   200. ltexp1dd
   201. exp11nnd
   202. mulsubdivbinom2
   203. muldivbinom2
   204. sq10
   205. sq10e99m1
   206. 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. hasheqf1oi
    23. hashf1rn
    24. hasheqf1od
    25. fz1eqb
    26. hashcard
    27. hashcl
    28. hashxrcl
    29. hashclb
    30. nfile
    31. hashvnfin
    32. hashnfinnn0
    33. isfinite4
    34. hasheq0
    35. hashneq0
    36. hashgt0n0
    37. hashnncl
    38. hash0
    39. hashelne0d
    40. hashsng
    41. hashen1
    42. hash1elsn
    43. hashrabrsn
    44. hashrabsn01
    45. hashrabsn1
    46. hashfn
    47. fseq1hash
    48. hashgadd
    49. hashgval2
    50. hashdom
    51. hashdomi
    52. hashsdom
    53. hashun
    54. hashun2
    55. hashun3
    56. hashinfxadd
    57. hashunx
    58. hashge0
    59. hashgt0
    60. hashge1
    61. 1elfz0hash
    62. hashnn0n0nn
    63. hashunsng
    64. hashunsngx
    65. hashunsnggt
    66. hashprg
    67. elprchashprn2
    68. hashprb
    69. hashprdifel
    70. prhash2ex
    71. hashle00
    72. hashgt0elex
    73. hashgt0elexb
    74. hashp1i
    75. hash1
    76. hash2
    77. hash3
    78. hash4
    79. pr0hash2ex
    80. hashss
    81. prsshashgt1
    82. hashin
    83. hashssdif
    84. hashdif
    85. hashdifsn
    86. hashdifpr
    87. hashsn01
    88. hashsnle1
    89. hashsnlei
    90. hash1snb
    91. euhash1
    92. hash1n0
    93. hashgt12el
    94. hashgt12el2
    95. hashgt23el
    96. hashunlei
    97. hashsslei
    98. hashfz
    99. fzsdom2
    100. hashfzo
    101. hashfzo0
    102. hashfzp1
    103. hashfz0
    104. hashxplem
    105. hashxp
    106. hashmap
    107. hashpw
    108. hashfun
    109. hashres
    110. hashreshashfun
    111. hashimarn
    112. hashimarni
    113. hashfundm
    114. hashf1dmrn
    115. hashf1dmcdm
    116. resunimafz0
    117. fnfz0hash
    118. ffz0hash
    119. fnfz0hashnn0
    120. ffzo0hash
    121. fnfzo0hash
    122. fnfzo0hashnn0
    123. hashbclem
    124. hashbc
    125. hashfacen
    126. hashf1lem1
    127. hashf1lem2
    128. hashf1
    129. hashfac
    130. leiso
    131. leisorel
    132. fz1isolem
    133. fz1iso
    134. ishashinf
    135. seqcoll
    136. seqcoll2
    137. phphashd
    138. phphashrd
    139. Proper unordered pairs and triples (sets of size 2 and 3)
    140. Functions with a domain containing at least two different elements
    141. Finite induction on the size of the first component of a binary relation