Metamath Proof Explorer

Table of Contents - 5.6. Elementary integer functions

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