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. 1eluzge0
48. 2eluzge0
49. 2eluzge1
50. 5eluz3
51. uzuzle23
52. uzuzle24
53. uzuzle34
54. uzuzle35
55. eluz2nn
56. eluz3nn
57. eluz4nn
58. eluz5nn
59. eluzge2nn0
60. eluz2n0
61. uz3m2nn
62. uznnssnn
63. raluz
64. raluz2
65. rexuz
66. rexuz2
67. 2rexuz
68. peano2uz
69. peano2uzs
70. peano2uzr
71. uzaddcl
72. nn0pzuz
73. uzind4
74. uzind4ALT
75. uzind4s
76. uzind4s2
77. uzind4i
78. uzwo
79. uzwo2
80. nnwo
81. nnwof
82. nnwos
83. indstr
84. eluznn0
85. eluznn
86. eluz2b1
87. eluz2gt1
88. eluz2b2
89. eluz2b3
90. uz2m1nn
91. 1nuz2
92. elnn1uz2
93. uz2mulcl
94. indstr2
95. uzinfi
96. nninf
97. nn0inf
98. infssuzle
99. infssuzcl
100. ublbneg
101. eqreznegel
102. supminf
103. lbzbi
104. zsupss
105. suprzcl2
106. suprzub
107. uzsupss
108. nn01to3
109. nn0ge2m1nnALT