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. 1pneg1e0
2. 0m0e0
3. 1m0e1
4. 0p1e1
5. fv0p1e1
6. 1p0e1
7. 1p1e2
8. 2m1e1
9. 1e2m1
10. 3m1e2
11. 4m1e3
12. 5m1e4
13. 6m1e5
14. 7m1e6
15. 8m1e7
16. 9m1e8
17. 2p2e4
18. 2times
19. times2
20. 2timesi
21. times2i
22. 2txmxeqx
23. 2div2e1
24. 2p1e3
25. 1p2e3
26. 1p2e3ALT
27. 3p1e4
28. 4p1e5
29. 5p1e6
30. 6p1e7
31. 7p1e8
32. 8p1e9
33. 3p2e5
34. 3p3e6
35. 4p2e6
36. 4p3e7
37. 4p4e8
38. 5p2e7
39. 5p3e8
40. 5p4e9
41. 6p2e8
42. 6p3e9
43. 7p2e9
44. 1t1e1
45. 2t1e2
46. 2t2e4
47. 3t1e3
48. 3t2e6
49. 3t3e9
50. 4t2e8
51. 2t0e0
52. 4div2e2
53. 1lt2
54. 2lt3
55. 1lt3
56. 3lt4
57. 2lt4
58. 1lt4
59. 4lt5
60. 3lt5
61. 2lt5
62. 1lt5
63. 5lt6
64. 4lt6
65. 3lt6
66. 2lt6
67. 1lt6
68. 6lt7
69. 5lt7
70. 4lt7
71. 3lt7
72. 2lt7
73. 1lt7
74. 7lt8
75. 6lt8
76. 5lt8
77. 4lt8
78. 3lt8
79. 2lt8
80. 1lt8
81. 8lt9
82. 7lt9
83. 6lt9
84. 5lt9
85. 4lt9
86. 3lt9
87. 2lt9
88. 1lt9
89. 0ne2
90. 1ne2
91. 1le2
92. 2cnne0
93. 2rene0
94. 1le3
95. neg1mulneg1e1
96. halfre
97. halfcn
98. halfgt0
99. halfge0
100. halflt1
101. 2halves
102. 1mhlfehlf
103. 8th4div3
104. halfthird
105. halfpm6th
106. it0e0
107. 2mulicn
108. 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. zgt0ge1
60. nnleltp1
61. nnltp1le
62. nnaddm1cl
63. nn0ltp1le
64. nn0leltp1
65. nn0ltlem1
66. nn0sub2
67. nn0lt10b
68. nn0lt2
69. nn0le2is012
70. nn0lem1lt
71. nnlem1lt
72. nnltlem1
73. nnm1ge0
74. nn0ge0div
75. zdiv
76. zdivadd
77. zdivmul
78. zextle
79. zextlt
80. recnz
81. btwnnz
82. gtndiv
83. halfnz
84. 3halfnz
85. suprzcl
86. prime
87. msqznn
88. zneo
89. nneo
90. nneoi
91. zeo
92. zeo2
93. peano2uz2
94. peano5uzi
95. peano5uzti
96. dfuzi
97. uzind
98. uzind2
99. uzind3
100. nn0ind
101. nn0indALT
102. nn0indd
103. fzind
104. fnn0ind
105. nn0ind-raph
106. zindd
107. fzindd
108. btwnz
109. zred
110. zcnd
111. znegcld
112. peano2zd
113. zaddcld
114. zsubcld
115. zmulcld
116. znnn0nn
117. zadd2cl
118. zriotaneg
119. 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. 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