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. 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