Metamath Proof Explorer

Table of Contents - 5.4.11. 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