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. 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. 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. sqsubswap
   57. sqcl
   58. sqmul
   59. sqeq0
   60. sqdiv
   61. sqdivid
   62. sqne0
   63. resqcl
   64. sqgt0
   65. sqn0rp
   66. nnsqcl
   67. zsqcl
   68. qsqcl
   69. sq11
   70. nn0sq11
   71. lt2sq
   72. le2sq
   73. le2sq2
   74. sqge0
   75. zsqcl2
   76. 0expd
   77. exp0d
   78. exp1d
   79. expeq0d
   80. sqvald
   81. sqcld
   82. sqeq0d
   83. expcld
   84. expp1d
   85. expaddd
   86. expmuld
   87. sqrecd
   88. expclzd
   89. expne0d
   90. expnegd
   91. exprecd
   92. expp1zd
   93. expm1d
   94. expsubd
   95. sqmuld
   96. sqdivd
   97. expdivd
   98. mulexpd
   99. znsqcld
   100. reexpcld
   101. expge0d
   102. expge1d
   103. ltexp2a
   104. expmordi
   105. rpexpmord
   106. expcan
   107. ltexp2
   108. leexp2
   109. leexp2a
   110. ltexp2r
   111. leexp2r
   112. leexp1a
   113. exple1
   114. expubnd
   115. sumsqeq0
   116. sqvali
   117. sqcli
   118. sqeq0i
   119. sqrecii
   120. sqmuli
   121. sqdivi
   122. resqcli
   123. sqgt0i
   124. sqge0i
   125. lt2sqi
   126. le2sqi
   127. sq11i
   128. sq0
   129. sq0i
   130. sq0id
   131. sq1
   132. neg1sqe1
   133. sq2
   134. sq3
   135. sq4e2t8
   136. cu2
   137. irec
   138. i2
   139. i3
   140. i4
   141. nnlesq
   142. iexpcyc
   143. expnass
   144. sqlecan
   145. subsq
   146. subsq2
   147. binom2i
   148. subsqi
   149. sqeqori
   150. subsq0i
   151. sqeqor
   152. binom2
   153. binom21
   154. binom2sub
   155. binom2sub1
   156. binom2subi
   157. mulbinom2
   158. binom3
   159. sq01
   160. zesq
   161. nnesq
   162. crreczi
   163. bernneq
   164. bernneq2
   165. bernneq3
   166. expnbnd
   167. expnlbnd
   168. expnlbnd2
   169. expmulnbnd
   170. digit2
   171. digit1
   172. modexp
   173. discr1
   174. discr
   175. expnngt1
   176. expnngt1b
   177. sqoddm1div8
   178. nnsqcld
   179. nnexpcld
   180. nn0expcld
   181. rpexpcld
   182. ltexp2rd
   183. reexpclzd
   184. resqcld
   185. sqge0d
   186. sqgt0d
   187. ltexp2d
   188. leexp2d
   189. expcand
   190. leexp2ad
   191. leexp2rd
   192. lt2sqd
   193. le2sqd
   194. sq11d
   195. mulsubdivbinom2
   196. muldivbinom2
   197. sq10
   198. sq10e99m1
   199. 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. hashfacenOLD
    125. hashf1lem1
    126. hashf1lem1OLD
    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