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. nnmtmip
10. nn2ge
11. nnge1
12. nngt1ne1
13. nnle1eq1
14. nngt0
15. nnnlt1
16. nnnle0
17. nnne0
18. nnneneg
19. 0nnn
20. 0nnnALT
21. nnne0ALT
22. nngt0i
23. nnne0i
24. nndivre
25. nnrecre
26. nnrecgt0
27. nnsub
28. nnsubi
29. nndiv
30. nndivtr
31. nnge1d
32. nngt0d
33. nnne0d
34. nnrecred
35. nnaddcld
36. nnmulcld
37. nndivred
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. 0ne1
18. 1m1e0
19. 2nn
20. 2re
21. 2cn
22. 2cnALT
23. 2ex
24. 2cnd
25. 3nn
26. 3re
27. 3cn
28. 3ex
29. 4nn
30. 4re
31. 4cn
32. 5nn
33. 5re
34. 5cn
35. 6nn
36. 6re
37. 6cn
38. 7nn
39. 7re
40. 7cn
41. 8nn
42. 8re
43. 8cn
44. 9nn
45. 9re
46. 9cn
47. 0le0
48. 0le2
49. 2pos
50. 2ne0
51. 3pos
52. 3ne0
53. 4pos
54. 4ne0
55. 5pos
56. 6pos
57. 7pos
58. 8pos
59. 9pos
Some properties of specific numbers
1. neg1cn
2. neg1rr
3. neg1ne0
4. neg1lt0
5. negneg1e1
6. 1pneg1e0
7. 0m0e0
8. 1m0e1
9. 0p1e1
10. fv0p1e1
11. 1p0e1
12. 1p1e2
13. 2m1e1
14. 1e2m1
15. 3m1e2
16. 4m1e3
17. 5m1e4
18. 6m1e5
19. 7m1e6
20. 8m1e7
21. 9m1e8
22. 2p2e4
23. 2times
24. times2
25. 2timesi
26. times2i
27. 2txmxeqx
28. 2div2e1
29. 2p1e3
30. 1p2e3
31. 1p2e3ALT
32. 3p1e4
33. 4p1e5
34. 5p1e6
35. 6p1e7
36. 7p1e8
37. 8p1e9
38. 3p2e5
39. 3p3e6
40. 4p2e6
41. 4p3e7
42. 4p4e8
43. 5p2e7
44. 5p3e8
45. 5p4e9
46. 6p2e8
47. 6p3e9
48. 7p2e9
49. 1t1e1
50. 2t1e2
51. 2t2e4
52. 3t1e3
53. 3t2e6
54. 3t3e9
55. 4t2e8
56. 2t0e0
57. 4d2e2
58. 1lt2
59. 2lt3
60. 1lt3
61. 3lt4
62. 2lt4
63. 1lt4
64. 4lt5
65. 3lt5
66. 2lt5
67. 1lt5
68. 5lt6
69. 4lt6
70. 3lt6
71. 2lt6
72. 1lt6
73. 6lt7
74. 5lt7
75. 4lt7
76. 3lt7
77. 2lt7
78. 1lt7
79. 7lt8
80. 6lt8
81. 5lt8
82. 4lt8
83. 3lt8
84. 2lt8
85. 1lt8
86. 8lt9
87. 7lt9
88. 6lt9
89. 5lt9
90. 4lt9
91. 3lt9
92. 2lt9
93. 1lt9
94. 0ne2
95. 1ne2
96. 1le2
97. 2cnne0
98. 2rene0
99. 1le3
100. neg1mulneg1e1
101. halfre
102. halfcn
103. halfgt0
104. halfge0
105. halflt1
106. 1mhlfehlf
107. 8th4div3
108. halfpm6th
109. it0e0
110. 2mulicn
111. 2muline0
Simple number properties
1. halfcl
2. rehalfcl
3. half0
4. 2halves
5. halfpos2
6. halfpos
7. halfnneg2
8. halfaddsubcl
9. halfaddsub
10. subhalfhalf
11. lt2halves
12. addltmul
13. nominpos
14. avglt1
15. avglt2
16. avgle1
17. avgle2
18. avgle
19. 2timesd
20. times2d
21. halfcld
22. 2halvesd
23. rehalfcld
24. lt2halvesd
25. rehalfcli
26. lt2addmuld
27. add1p1
28. sub1m1
29. cnm2m1cnm3
30. xp1d2m1eqxm1d2
31. 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. nn0le2xi
56. nn0lele2xi
57. frnnn0supp
58. frnnn0fsupp
59. frnnn0suppg
60. frnnn0fsuppg
61. nnnn0d
62. nn0red
63. nn0cnd
64. nn0ge0d
65. nn0addcld
66. nn0mulcld
67. nn0readdcl
68. nn0n0n1ge2
69. nn0n0n1ge2b
70. nn0ge2m1nn
71. nn0ge2m1nn0
72. 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. nnssz
23. nn0ssz
24. nnz
25. nn0z
26. nnzi
27. nn0zi
28. elnnz1
29. znnnlt1
30. nnzrab
31. nn0zrab
32. 1z
33. 1zzd
34. 2z
35. 3z
36. 4z
37. znegcl
38. neg1z
39. znegclb
40. nn0negz
41. nn0negzi
42. zaddcl
43. peano2z
44. zsubcl
45. peano2zm
46. zletr
47. zrevaddcl
48. znnsub
49. znn0sub
50. nzadd
51. zmulcl
52. zltp1le
53. zleltp1
54. zlem1lt
55. zltlem1
56. zgt0ge1
57. nnleltp1
58. nnltp1le
59. nnaddm1cl
60. nn0ltp1le
61. nn0leltp1
62. nn0ltlem1
63. nn0sub2
64. nn0lt10b
65. nn0lt2
66. nn0le2is012
67. nn0lem1lt
68. nnlem1lt
69. nnltlem1
70. nnm1ge0
71. nn0ge0div
72. zdiv
73. zdivadd
74. zdivmul
75. zextle
76. zextlt
77. recnz
78. btwnnz
79. gtndiv
80. halfnz
81. 3halfnz
82. suprzcl
83. prime
84. msqznn
85. zneo
86. nneo
87. nneoi
88. zeo
89. zeo2
90. peano2uz2
91. peano5uzi
92. peano5uzti
93. dfuzi
94. uzind
95. uzind2
96. uzind3
97. nn0ind
98. nn0indALT
99. nn0indd
100. fzind
101. fnn0ind
102. nn0ind-raph
103. zindd
104. btwnz
105. nn0zd
106. nnzd
107. zred
108. zcnd
109. znegcld
110. peano2zd
111. zaddcld
112. zsubcld
113. zmulcld
114. znnn0nn
115. zadd2cl
116. zriotaneg
117. 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. 10nn
18. 10pos
19. 10nn0
20. 10re
21. decnncl
22. dec0u
23. dec0h
24. numnncl2
25. decnncl2
26. numlt
27. numltc
28. le9lt10
29. declt
30. decltc
31. declth
32. decsuc
33. 3declth
34. 3decltc
35. decle
36. decleh
37. declei
38. numlti
39. declti
40. decltdi
41. numsucc
42. decsucc
43. 1e0p1
44. dec10p
45. numma
46. nummac
47. numma2c
48. numadd
49. numaddc
50. nummul1c
51. nummul2c
52. decma
53. decmac
54. decma2c
55. decadd
56. decaddc
57. decaddc2
58. decrmanc
59. decrmac
60. decaddm10
61. decaddi
62. decaddci
63. decaddci2
64. decsubi
65. decmul1
66. decmul1c
67. decmul2c
68. decmulnc
69. 11multnc
70. decmul10add
71. 6p5lem
72. 5p5e10
73. 6p4e10
74. 6p5e11
75. 6p6e12
76. 7p3e10
77. 7p4e11
78. 7p5e12
79. 7p6e13
80. 7p7e14
81. 8p2e10
82. 8p3e11
83. 8p4e12
84. 8p5e13
85. 8p6e14
86. 8p7e15
87. 8p8e16
88. 9p2e11
89. 9p3e12
90. 9p4e13
91. 9p5e14
92. 9p6e15
93. 9p7e16
94. 9p8e17
95. 9p9e18
96. 10p10e20
97. 10m1e9
98. 4t3lem
99. 4t3e12
100. 4t4e16
101. 5t2e10
102. 5t3e15
103. 5t4e20
104. 5t5e25
105. 6t2e12
106. 6t3e18
107. 6t4e24
108. 6t5e30
109. 6t6e36
110. 7t2e14
111. 7t3e21
112. 7t4e28
113. 7t5e35
114. 7t6e42
115. 7t7e49
116. 8t2e16
117. 8t3e24
118. 8t4e32
119. 8t5e40
120. 8t6e48
121. 8t7e56
122. 8t8e64
123. 9t2e18
124. 9t3e27
125. 9t4e36
126. 9t5e45
127. 9t6e54
128. 9t7e63
129. 9t8e72
130. 9t9e81
131. 9t11e99
132. 9lt10
133. 8lt10
134. 7lt10
135. 6lt10
136. 5lt10
137. 4lt10
138. 3lt10
139. 2lt10
140. 1lt10
141. decbin0
142. decbin2
143. decbin3
144. halfthird
145. 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. eluzaddi
31. eluzsubi
32. eluzadd
33. eluzsub
34. subeluzsub
35. uzm1
36. uznn0sub
37. uzin
38. uzp1
39. nn0uz
40. nnuz
41. elnnuz
42. elnn0uz
43. eluz2nn
44. eluz4eluz2
45. eluz4nn
46. eluzge2nn0
47. eluz2n0
48. uzuzle23
49. eluzge3nn
50. uz3m2nn
51. 1eluzge0
52. 2eluzge0
53. 2eluzge1
54. uznnssnn
55. raluz
56. raluz2
57. rexuz
58. rexuz2
59. 2rexuz
60. peano2uz
61. peano2uzs
62. peano2uzr
63. uzaddcl
64. nn0pzuz
65. uzind4
66. uzind4ALT
67. uzind4s
68. uzind4s2
69. uzind4i
70. uzwo
71. uzwo2
72. nnwo
73. nnwof
74. nnwos
75. indstr
76. eluznn0
77. eluznn
78. eluz2b1
79. eluz2gt1
80. eluz2b2
81. eluz2b3
82. uz2m1nn
83. 1nuz2
84. elnn1uz2
85. uz2mulcl
86. indstr2
87. uzinfi
88. nninf
89. nn0inf
90. infssuzle
91. infssuzcl
92. ublbneg
93. eqreznegel
94. supminf
95. lbzbi
96. zsupss
97. suprzcl2
98. suprzub
99. uzsupss
100. nn01to3
101. 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. addex
13. mulex