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. 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