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. eluzadd
31. eluzsub
32. eluzaddi
33. eluzaddiOLD
34. eluzsubi
35. eluzsubiOLD
36. eluzaddOLD
37. eluzsubOLD
38. subeluzsub
39. uzm1
40. uznn0sub
41. uzin
42. uzp1
43. nn0uz
44. nnuz
45. elnnuz
46. elnn0uz
47. eluz2nn
48. eluz4eluz2
49. eluz4eluz3
50. 5eluz3
51. eluz4nn
52. eluzge2nn0
53. eluz2n0
54. uzuzle23
55. eluzge3nn
56. uz3m2nn
57. 1eluzge0
58. 2eluzge0
59. 2eluzge1
60. uznnssnn
61. raluz
62. raluz2
63. rexuz
64. rexuz2
65. 2rexuz
66. peano2uz
67. peano2uzs
68. peano2uzr
69. uzaddcl
70. nn0pzuz
71. uzind4
72. uzind4ALT
73. uzind4s
74. uzind4s2
75. uzind4i
76. uzwo
77. uzwo2
78. nnwo
79. nnwof
80. nnwos
81. indstr
82. eluznn0
83. eluznn
84. eluz2b1
85. eluz2gt1
86. eluz2b2
87. eluz2b3
88. uz2m1nn
89. 1nuz2
90. elnn1uz2
91. uz2mulcl
92. indstr2
93. uzinfi
94. nninf
95. nn0inf
96. infssuzle
97. infssuzcl
98. ublbneg
99. eqreznegel
100. supminf
101. lbzbi
102. zsupss
103. suprzcl2
104. suprzub
105. uzsupss
106. nn01to3
107. nn0ge2m1nnALT