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