Metamath Proof Explorer

Table of Contents - 5.4. Integer sets

Positive integers (as a subset of complex numbers)
1. cn
2. df-nn
3. nnexALT
4. peano5nni
5. nnssre
6. nnsscn
7. nnex
8. nnre
9. nncn
10. nnrei
11. nncni
12. 1nn
13. peano2nn
14. dfnn2
15. dfnn3
16. nnred
17. nncnd
18. peano2nnd
Principle of mathematical induction
1. nnind
2. nnindALT
3. nnindd
4. nn1m1nn
5. nn1suc
6. nnaddcl
7. nnmulcl
8. nnmulcli
9. nnadd1com
10. nnaddcom
11. nnaddcomli
12. nnmtmip
13. nn2ge
14. nnge1
15. nngt1ne1
16. nnle1eq1
17. nngt0
18. nnnlt1
19. nnnle0
20. nnne0
21. nnneneg
22. 0nnn
23. 0nnnALT
24. nnne0ALT
25. nngt0i
26. nnne0i
27. nndivre
28. nnrecre
29. nnrecgt0
30. nnsub
31. nnsubi
32. nndiv
33. nndivtr
34. nnge1d
35. nngt0d
36. nnne0d
37. nnrecred
38. nnaddcld
39. nnmulcld
40. nndivred
41. 1t1e1ALT
42. nnadddir
43. nnmul1com
44. nnmulcom
Decimal representation of numbers
1. c2
2. c3
3. c4
4. c5
5. c6
6. c7
7. c8
8. c9
9. df-2
10. df-3
11. df-4
12. df-5
13. df-6
14. df-7
15. df-8
16. df-9
17. 1eltp012
18. 0ne1
19. 1m1e0
20. 2nn
21. 2re
22. 2cn
23. 2cnALT
24. 2ex
25. 2cnd
26. 3nn
27. 3re
28. 3cn
29. 3ex
30. 4nn
31. 4re
32. 4cn
33. 5nn
34. 5re
35. 5cn
36. 6nn
37. 6re
38. 6cn
39. 7nn
40. 7re
41. 7cn
42. 8nn
43. 8re
44. 8cn
45. 9nn
46. 9re
47. 9cn
48. 0le0
49. 0le2
50. 0le2OLD
51. 2pos
52. 2posOLD
53. 2ne0
54. 2thalfe1
55. 3pos
56. 3ne0
57. 4pos
58. 4ne0
59. 5pos
60. 6pos
61. 7pos
62. 8pos
63. 9pos
Some properties of specific numbers
1. 1pneg1e0
2. 0m0e0
3. 1m0e1
4. 0p1e1
5. fv0p1e1
6. 1p0e1
7. 1p1e2
8. 2m1e1
9. 2m1e1OLD
10. 1e2m1
11. 3m1e2
12. 4m1e3
13. 5m1e4
14. 6m1e5
15. 7m1e6
16. 8m1e7
17. 9m1e8
18. 2p2e4
19. 2times
20. times2
21. 2timesi
22. times2i
23. 2txmxeqx
24. 2div2e1
25. 2p1e3
26. 1p2e3
27. 1p2e3ALT
28. 3p1e4
29. 4p1e5
30. 5p1e6
31. 6p1e7
32. 7p1e8
33. 8p1e9
34. 3p2e5
35. 3p3e6
36. 4p2e6
37. 4p3e7
38. 4p4e8
39. 5p2e7
40. 5p3e8
41. 5p4e9
42. 6p2e8
43. 6p3e9
44. 7p2e9
45. 1t1e1
46. 2t1e2
47. 2t2e4
48. 3t1e3
49. 3t2e6
50. 2t3e6
51. 3t3e9
52. 4t2e8
53. 2t4e8
54. 2t0e0
55. 4div2e2
56. 1lt2
57. 2lt3
58. 2le3
59. 1lt3
60. 3lt4
61. 2lt4
62. 1lt4
63. 4lt5
64. 3lt5
65. 2lt5
66. 1lt5
67. 5lt6
68. 4lt6
69. 3lt6
70. 2lt6
71. 1lt6
72. 6lt7
73. 5lt7
74. 4lt7
75. 3lt7
76. 2lt7
77. 1lt7
78. 7lt8
79. 6lt8
80. 5lt8
81. 4lt8
82. 3lt8
83. 2lt8
84. 1lt8
85. 8lt9
86. 7lt9
87. 6lt9
88. 5lt9
89. 4lt9
90. 3lt9
91. 2lt9
92. 1lt9
93. 0ne2
94. 1ne2
95. 1le2
96. 2cnne0
97. 2rene0
98. 1le3
99. neg1mulneg1e1
100. halfre
101. halfcn
102. halfgt0
103. halfge0
104. halflt1
105. 2halves
106. 1mhlfehlf
107. 8th4div3
108. halfthird
109. halfpm6th
110. it0e0
111. 2mulicn
112. 2muline0
Simple number properties
1. halfcl
2. rehalfcl
3. half0
4. halfpos2
5. halfpos
6. halfnneg2
7. halfaddsubcl
8. halfaddsub
9. subhalfhalf
10. lt2halves
11. addltmul
12. nominpos
13. avglt1
14. avglt2
15. avgle1
16. avgle2
17. avgle
18. 2timesd
19. times2d
20. halfcld
21. 2halvesd
22. rehalfcld
23. lt2halvesd
24. rehalfcli
25. lt2addmuld
26. add1p1
27. sub1m1
28. cnm2m1cnm3
29. xp1d2m1eqxm1d2
30. div4p1lem1div2
The Archimedean property
1. nnunb
2. arch
3. nnrecl
4. bndndx
Nonnegative integers (as a subset of complex numbers)
1. cn0
2. df-n0
3. elnn0
4. nnssnn0
5. nn0ssre
6. nn0sscn
7. nn0ex
8. nnnn0
9. nnnn0i
10. nn0re
11. nn0cn
12. nn0rei
13. nn0cni
14. dfn2
15. elnnne0
16. 0nn0
17. 1nn0
18. 2nn0
19. 3nn0
20. 4nn0
21. 5nn0
22. 6nn0
23. 7nn0
24. 8nn0
25. 9nn0
26. nn0ge0
27. nn0nlt0
28. nn0ge0i
29. nn0le0eq0
30. nn0p1gt0
31. nnnn0addcl
32. nn0nnaddcl
33. 0mnnnnn0
34. un0addcl
35. un0mulcl
36. nn0addcl
37. nn0mulcl
38. nn0addcli
39. nn0mulcli
40. nn0p1nn
41. peano2nn0
42. nnm1nn0
43. elnn0nn
44. elnnnn0
45. elnnnn0b
46. elnnnn0c
47. nn0addge1
48. nn0addge2
49. nn0addge1i
50. nn0addge2i
51. nn0sub
52. ltsubnn0
53. nn0negleid
54. difgtsumgt
55. nn0le2x
56. nn0le2xi
57. nn0lele2xi
58. fcdmnn0supp
59. fcdmnn0fsupp
60. fcdmnn0suppg
61. fcdmnn0fsuppg
62. nnnn0d
63. nn0red
64. nn0cnd
65. nn0ge0d
66. nn0addcld
67. nn0mulcld
68. nn0readdcl
69. nn0n0n1ge2
70. nn0n0n1ge2b
71. nn0ge2m1nn
72. nn0ge2m1nn0
73. nn0nndivcl
Extended nonnegative integers
1. cxnn0
2. df-xnn0
3. elxnn0
4. nn0ssxnn0
5. nn0xnn0
6. xnn0xr
7. 0xnn0
8. pnf0xnn0
9. nn0nepnf
10. nn0xnn0d
11. nn0nepnfd
12. xnn0nemnf
13. xnn0xrnemnf
14. xnn0nnn0pnf
Integers (as a subset of complex numbers)
1. cz
2. df-z
3. elz
4. nnnegz
5. zre
6. zcn
7. zrei
8. zssre
9. zsscn
10. zex
11. elnnz
12. 0z
13. 0zd
14. elnn0z
15. elznn0nn
16. elznn0
17. elznn
18. zle0orge1
19. elz2
20. dfz2
21. zexALT
22. nnz
23. nnssz
24. nn0ssz
25. nn0z
26. nn0zd
27. nnzd
28. nnzi
29. nn0zi
30. elnnz1
31. znnnlt1
32. nnzrab
33. nn0zrab
34. 1z
35. 1zzd
36. 2z
37. 3z
38. 4z
39. znegcl
40. neg1z
41. znegclb
42. nn0negz
43. nn0negzi
44. zaddcl
45. peano2z
46. zsubcl
47. peano2zm
48. zletr
49. zrevaddcl
50. znnsub
51. znn0sub
52. nzadd
53. zmulcl
54. zltp1le
55. zleltp1
56. zlem1lt
57. zltlem1
58. zltlem1d
59. zltp1led
60. zgt0ge1
61. nnleltp1
62. nnltp1le
63. nnaddm1cl
64. nn0ltp1le
65. nn0leltp1
66. nn0ltlem1
67. nn0sub2
68. nn0lt10b
69. nn0lt2
70. nn0le2is012
71. nn0lem1lt
72. nnlem1lt
73. nnltlem1
74. nnm1ge0
75. nn0ge0div
76. zdiv
77. zdivadd
78. zdivmul
79. zextle
80. zextlt
81. recnz
82. btwnnz
83. gtndiv
84. halfnz
85. 3halfnz
86. suprzcl
87. prime
88. msqznn
89. zneo
90. nneo
91. nneoi
92. zeo
93. zeo2
94. peano2uz2
95. peano5uzi
96. peano5uzti
97. dfuzi
98. uzind
99. uzind2
100. uzind3
101. nn0ind
102. nn0indALT
103. nn0indd
104. fzind
105. fnn0ind
106. nn0ind-raph
107. zindd
108. fzindd
109. btwnz
110. zred
111. zcnd
112. znegcld
113. peano2zd
114. zaddcld
115. zsubcld
116. zmulcld
117. znnn0nn
118. zadd2cl
119. zriotaneg
120. suprfinzcl
Decimal arithmetic
1. cdc
2. df-dec
3. 9p1e10
4. dfdec10
5. decex
6. deceq1
7. deceq2
8. deceq1i
9. deceq2i
10. deceq12i
11. numnncl
12. num0u
13. num0h
14. numcl
15. numsuc
16. deccl
17. 11nn0
18. 12nn0
19. 16nn0
20. 25nn0
21. 10nn
22. 10pos
23. 10nn0
24. 10re
25. decnncl
26. 11nn
27. dec0u
28. dec0h
29. numnncl2
30. decnncl2
31. numlt
32. numltc
33. le9lt10
34. declt
35. decltc
36. declth
37. decsuc
38. 3declth
39. 3decltc
40. decle
41. decleh
42. declei
43. numlti
44. declti
45. decltdi
46. numsucc
47. decsucc
48. 1e0p1
49. dec10p
50. numma
51. nummac
52. numma2c
53. numadd
54. numaddc
55. nummul1c
56. nummul2c
57. decma
58. decmac
59. decma2c
60. decadd
61. decaddc
62. decaddc2
63. decrmanc
64. decrmac
65. decaddm10
66. decaddi
67. decaddci
68. decaddci2
69. decsubi
70. decmul1
71. decmul1c
72. decmul2c
73. decmulnc
74. 11multnc
75. decmul10add
76. 6p5lem
77. 5p5e10
78. 6p4e10
79. 6p5e11
80. 6p6e12
81. 7p3e10
82. 7p4e11
83. 7p5e12
84. 7p6e13
85. 7p7e14
86. 8p2e10
87. 8p3e11
88. 8p4e12
89. 8p5e13
90. 8p6e14
91. 8p7e15
92. 8p8e16
93. 9p2e11
94. 9p3e12
95. 9p4e13
96. 9p5e14
97. 9p6e15
98. 9p7e16
99. 9p8e17
100. 9p9e18
101. 10p10e20
102. 10m1e9
103. 4t3lem
104. 4t3e12
105. 4t4e16
106. 5t2e10
107. 5t3e15
108. 5t4e20
109. 5t5e25
110. 6t2e12
111. 6t3e18
112. 6t4e24
113. 6t5e30
114. 6t6e36
115. 7t2e14
116. 7t3e21
117. 7t4e28
118. 7t5e35
119. 7t6e42
120. 7t7e49
121. 8t2e16
122. 8t3e24
123. 8t4e32
124. 8t5e40
125. 8t6e48
126. 8t7e56
127. 8t8e64
128. 9t2e18
129. 9t3e27
130. 9t4e36
131. 9t5e45
132. 9t6e54
133. 9t7e63
134. 9t8e72
135. 9t9e81
136. 9t11e99
137. 9t11e99OLD
138. 9lt10
139. 8lt10
140. 7lt10
141. 6lt10
142. 5lt10
143. 4lt10
144. 3lt10
145. 2lt10
146. 1lt10
147. 1lt10OLD
148. decbin0
149. decbin2
150. decbin3
151. 5recm6rec
Upper sets of integers
1. cuz
2. df-uz
3. uzval
4. uzf
5. eluz1
6. eluzel2
7. eluz2
8. eluzmn
9. eluz1i
10. eluzuzle
11. eluzelz
12. eluzelre
13. eluzelcn
14. eluzle
15. eluz
16. uzid
17. uzidd
18. uzn0
19. uztrn
20. uztrn2
21. uzneg
22. uzssz
23. uzssre
24. uzss
25. uztric
26. uz11
27. eluzp1m1
28. eluzp1l
29. eluzp1p1
30. eluzadd
31. eluzsub
32. eluzaddi
33. eluzsubi
34. subeluzsub
35. uzm1
36. uznn0sub
37. uzin
38. uzp1
39. nn0uz
40. nnuz
41. elnnuz
42. elnn0uz
43. 1eluzge0
44. 2eluzge0
45. 2eluzge1
46. 5eluz3
47. uzuzle23
48. uzuzle24
49. uzuzle34
50. uzuzle35
51. eluz2nn
52. eluz3nn
53. eluz4nn
54. eluz5nn
55. eluzge2nn0
56. eluz2n0
57. uz3m2nn
58. uznnssnn
59. raluz
60. raluz2
61. rexuz
62. rexuz2
63. 2rexuz
64. peano2uz
65. peano2uzs
66. peano2uzr
67. uzaddcl
68. nn0pzuz
69. uzind4
70. uzind4ALT
71. uzind4s
72. uzind4s2
73. uzind4i
74. uzwo
75. uzwo2
76. nnwo
77. nnwof
78. nnwos
79. indstr
80. eluznn0
81. eluznn
82. eluz2b1
83. eluz2gt1
84. eluz2b2
85. eluz2b3
86. uz2m1nn
87. 1nuz2
88. elnn1uz2
89. uz2mulcl
90. indstr2
91. uzinfi
92. nninf
93. nn0inf
94. infssuzle
95. infssuzcl
96. ublbneg
97. eqreznegel
98. supminf
99. lbzbi
100. zsupss
101. suprzcl2
102. suprzub
103. uzsupss
104. nn01to3
105. nn0ge2m1nnALT
Well-ordering principle for bounded-below sets of integers
1. uzwo3
2. zmin
3. zmax
4. zbtwnre
5. rebtwnz
Rational numbers (as a subset of complex numbers)
1. cq
2. df-q
3. elq
4. qmulz
5. znq
6. qre
7. zq
8. qred
9. zssq
10. nn0ssq
11. nnssq
12. qssre
13. qsscn
14. qex
15. nnq
16. qcn
17. qexALT
18. qaddcl
19. qnegcl
20. qmulcl
21. qsubcl
22. qreccl
23. qdivcl
24. qrevaddcl
25. nnrecq
26. irradd
27. irrmul
28. elpq
29. elpqb
Existence of the set of complex numbers
1. rpnnen1lem2
2. rpnnen1lem1
3. rpnnen1lem3
4. rpnnen1lem4
5. rpnnen1lem5
6. rpnnen1lem6
7. rpnnen1
8. reexALT
9. cnref1o
10. cnexALT
11. xrex
12. mpoaddex
13. addex
14. mpomulex
15. mulex