Metamath Proof Explorer

Table of Contents - 5.5. Order sets

Positive reals (as a subset of complex numbers)
1. crp
2. df-rp
3. elrp
4. elrpii
5. 1rp
6. 2rp
7. 3rp
8. rpssre
9. rpre
10. rpxr
11. rpcn
12. nnrp
13. rpgt0
14. rpge0
15. rpregt0
16. rprege0
17. rpne0
18. rprene0
19. rpcnne0
20. rpcndif0
21. ralrp
22. rexrp
23. rpaddcl
24. rpmulcl
25. rpmtmip
26. rpdivcl
27. rpreccl
28. rphalfcl
29. rpgecl
30. rphalflt
31. rerpdivcl
32. ge0p1rp
33. rpneg
34. negelrp
35. negelrpd
36. 0nrp
37. ltsubrp
38. ltaddrp
39. difrp
40. elrpd
41. nnrpd
42. zgt1rpn0n1
43. rpred
44. rpxrd
45. rpcnd
46. rpgt0d
47. rpge0d
48. rpne0d
49. rpregt0d
50. rprege0d
51. rprene0d
52. rpcnne0d
53. rpreccld
54. rprecred
55. rphalfcld
56. reclt1d
57. recgt1d
58. rpaddcld
59. rpmulcld
60. rpdivcld
61. ltrecd
62. lerecd
63. ltrec1d
64. lerec2d
65. lediv2ad
66. ltdiv2d
67. lediv2d
68. ledivdivd
69. divge1
70. divlt1lt
71. divle1le
72. ledivge1le
73. ge0p1rpd
74. rerpdivcld
75. ltsubrpd
76. ltaddrpd
77. ltaddrp2d
78. ltmulgt11d
79. ltmulgt12d
80. gt0divd
81. ge0divd
82. rpgecld
83. divge0d
84. ltmul1d
85. ltmul2d
86. lemul1d
87. lemul2d
88. ltdiv1d
89. lediv1d
90. ltmuldivd
91. ltmuldiv2d
92. lemuldivd
93. lemuldiv2d
94. ltdivmuld
95. ltdivmul2d
96. ledivmuld
97. ledivmul2d
98. ltmul1dd
99. ltmul2dd
100. ltdiv1dd
101. lediv1dd
102. lediv12ad
103. mul2lt0rlt0
104. mul2lt0rgt0
105. mul2lt0llt0
106. mul2lt0lgt0
107. mul2lt0bi
108. prodge0rd
109. prodge0ld
110. ltdiv23d
111. lediv23d
112. lt2mul2divd
113. nnledivrp
114. nn0ledivnn
115. addlelt
Infinity and the extended real number system (cont.)
1. cxne
2. cxad
3. cxmu
4. df-xneg
5. df-xadd
6. df-xmul
7. ltxr
8. elxr
9. xrnemnf
10. xrnepnf
11. xrltnr
12. ltpnf
13. ltpnfd
14. 0ltpnf
15. mnflt
16. mnfltd
17. mnflt0
18. mnfltpnf
19. mnfltxr
20. pnfnlt
21. nltmnf
22. pnfge
23. xnn0n0n1ge2b
24. 0lepnf
25. xnn0ge0
26. mnfle
27. xrltnsym
28. xrltnsym2
29. xrlttri
30. xrlttr
31. xrltso
32. xrlttri2
33. xrlttri3
34. xrleloe
35. xrleltne
36. xrltlen
37. dfle2
38. dflt2
39. xrltle
40. xrltled
41. xrleid
42. xrleidd
43. xrletri
44. xrletri3
45. xrletrid
46. xrlelttr
47. xrltletr
48. xrletr
49. xrlttrd
50. xrlelttrd
51. xrltletrd
52. xrletrd
53. xrltne
54. nltpnft
55. xgepnf
56. ngtmnft
57. xlemnf
58. xrrebnd
59. xrre
60. xrre2
61. xrre3
62. ge0gtmnf
63. ge0nemnf
64. xrrege0
65. xrmax1
66. xrmax2
67. xrmin1
68. xrmin2
69. xrmaxeq
70. xrmineq
71. xrmaxlt
72. xrltmin
73. xrmaxle
74. xrlemin
75. max1
76. max1ALT
77. max2
78. 2resupmax
79. min1
80. min2
81. maxle
82. lemin
83. maxlt
84. ltmin
85. lemaxle
86. max0sub
87. ifle
88. z2ge
89. qbtwnre
90. qbtwnxr
91. qsqueeze
92. qextltlem
93. qextlt
94. qextle
95. xralrple
96. alrple
97. xnegeq
98. xnegex
99. xnegpnf
100. xnegmnf
101. rexneg
102. xneg0
103. xnegcl
104. xnegneg
105. xneg11
106. xltnegi
107. xltneg
108. xleneg
109. xlt0neg1
110. xlt0neg2
111. xle0neg1
112. xle0neg2
113. xaddval
114. xaddf
115. xmulval
116. xaddpnf1
117. xaddpnf2
118. xaddmnf1
119. xaddmnf2
120. pnfaddmnf
121. mnfaddpnf
122. rexadd
123. rexsub
124. rexaddd
125. xnn0xaddcl
126. xaddnemnf
127. xaddnepnf
128. xnegid
129. xaddcl
130. xaddcom
131. xaddid1
132. xaddid2
133. xaddid1d
134. xnn0lem1lt
135. xnn0lenn0nn0
136. xnn0le2is012
137. xnn0xadd0
138. xnegdi
139. xaddass
140. xaddass2
141. xpncan
142. xnpcan
143. xleadd1a
144. xleadd2a
145. xleadd1
146. xltadd1
147. xltadd2
148. xaddge0
149. xle2add
150. xlt2add
151. xsubge0
152. xposdif
153. xlesubadd
154. xmullem
155. xmullem2
156. xmulcom
157. xmul01
158. xmul02
159. xmulneg1
160. xmulneg2
161. rexmul
162. xmulf
163. xmulcl
164. xmulpnf1
165. xmulpnf2
166. xmulmnf1
167. xmulmnf2
168. xmulpnf1n
169. xmulid1
170. xmulid2
171. xmulm1
172. xmulasslem2
173. xmulgt0
174. xmulge0
175. xmulasslem
176. xmulasslem3
177. xmulass
178. xlemul1a
179. xlemul2a
180. xlemul1
181. xlemul2
182. xltmul1
183. xltmul2
184. xadddilem
185. xadddi
186. xadddir
187. xadddi2
188. xadddi2r
189. x2times
190. xnegcld
191. xaddcld
192. xmulcld
193. xadd4d
194. xnn0add4d
Supremum and infimum on the extended reals
1. xrsupexmnf
2. xrinfmexpnf
3. xrsupsslem
4. xrinfmsslem
5. xrsupss
6. xrinfmss
7. xrinfmss2
8. xrub
9. supxr
10. supxr2
11. supxrcl
12. supxrun
13. supxrmnf
14. supxrpnf
15. supxrunb1
16. supxrunb2
17. supxrbnd1
18. supxrbnd2
19. xrsup0
20. supxrub
21. supxrlub
22. supxrleub
23. supxrre
24. supxrbnd
25. supxrgtmnf
26. supxrre1
27. supxrre2
28. supxrss
29. infxrcl
30. infxrlb
31. infxrgelb
32. infxrre
33. infxrmnf
34. xrinf0
35. infxrss
36. reltre
37. rpltrp
38. reltxrnmnf
39. infmremnf
40. infmrp1
Real number intervals
1. cioo
2. cioc
3. cico
4. cicc
5. df-ioo
6. df-ioc
7. df-ico
8. df-icc
9. ixxval
10. elixx1
11. ixxf
12. ixxex
13. ixxssxr
14. elixx3g
15. ixxssixx
16. ixxdisj
17. ixxun
18. ixxin
19. ixxss1
20. ixxss2
21. ixxss12
22. ixxub
23. ixxlb
24. iooex
25. iooval
26. ioo0
27. ioon0
28. ndmioo
29. iooid
30. elioo3g
31. elioore
32. lbioo
33. ubioo
34. iooval2
35. iooin
36. iooss1
37. iooss2
38. iocval
39. icoval
40. iccval
41. elioo1
42. elioo2
43. elioc1
44. elico1
45. elicc1
46. iccid
47. ico0
48. ioc0
49. icc0
50. dfrp2
51. elicod
52. icogelb
53. elicore
54. ubioc1
55. lbico1
56. iccleub
57. iccgelb
58. elioo5
59. eliooxr
60. eliooord
61. elioo4g
62. ioossre
63. ioosscn
64. elioc2
65. elico2
66. elicc2
67. elicc2i
68. elicc4
69. iccss
70. iccssioo
71. icossico
72. iccss2
73. iccssico
74. iccssioo2
75. iccssico2
76. ioomax
77. iccmax
78. ioopos
79. ioorp
80. iooshf
81. iocssre
82. icossre
83. iccssre
84. iccssxr
85. iocssxr
86. icossxr
87. ioossicc
88. iccssred
89. eliccxr
90. icossicc
91. iocssicc
92. ioossico
93. iocssioo
94. icossioo
95. ioossioo
96. iccsupr
97. elioopnf
98. elioomnf
99. elicopnf
100. repos
101. ioof
102. iccf
103. unirnioo
104. dfioo2
105. ioorebas
106. xrge0neqmnf
107. xrge0nre
108. elrege0
109. nn0rp0
110. rge0ssre
111. elxrge0
112. 0e0icopnf
113. 0e0iccpnf
114. ge0addcl
115. ge0mulcl
116. ge0xaddcl
117. ge0xmulcl
118. lbicc2
119. ubicc2
120. elicc01
121. elunitrn
122. elunitcn
123. 0elunit
124. 1elunit
125. iooneg
126. iccneg
127. icoshft
128. icoshftf1o
129. icoun
130. icodisj
131. ioounsn
132. snunioo
133. snunico
134. snunioc
135. prunioo
136. ioodisj
137. ioojoin
138. difreicc
139. iccsplit
140. iccshftr
141. iccshftri
142. iccshftl
143. iccshftli
144. iccdil
145. iccdili
146. icccntr
147. icccntri
148. divelunit
149. lincmb01cmp
150. iccf1o
151. iccen
152. xov1plusxeqvd
153. unitssre
154. unitsscn
155. supicc
156. supiccub
157. supicclub
158. supicclub2
159. zltaddlt1le
160. xnn0xrge0
Finite intervals of integers
1. cfz
2. df-fz
3. fzval
4. fzval2
5. fzf
6. elfz1
7. elfz
8. elfz2
9. elfzd
10. elfz5
11. elfz4
12. elfzuzb
13. eluzfz
14. elfzuz
15. elfzuz3
16. elfzel2
17. elfzel1
18. elfzelz
19. elfzelzd
20. fzssz
21. elfzle1
22. elfzle2
23. elfzuz2
24. elfzle3
25. eluzfz1
26. eluzfz2
27. eluzfz2b
28. elfz3
29. elfz1eq
30. elfzubelfz
31. peano2fzr
32. fzn0
33. fz0
34. fzn
35. fzen
36. fz1n
37. 0nelfz1
38. 0fz1
39. fz10
40. uzsubsubfz
41. uzsubsubfz1
42. ige3m2fz
43. fzsplit2
44. fzsplit
45. fzdisj
46. fz01en
47. elfznn
48. elfz1end
49. fz1ssnn
50. fznn0sub
51. fzmmmeqm
52. fzaddel
53. fzadd2
54. fzsubel
55. fzopth
56. fzass4
57. fzss1
58. fzss2
59. fzssuz
60. fzsn
61. fzssp1
62. fzssnn
63. ssfzunsnext
64. ssfzunsn
65. fzsuc
66. fzpred
67. fzpreddisj
68. elfzp1
69. fzp1ss
70. fzelp1
71. fzp1elp1
72. fznatpl1
73. fzpr
74. fztp
75. fz12pr
76. fzsuc2
77. fzp1disj
78. fzdifsuc
79. fzprval
80. fztpval
81. fzrev
82. fzrev2
83. fzrev2i
84. fzrev3
85. fzrev3i
86. fznn
87. elfz1b
88. elfz1uz
89. elfzm11
90. uzsplit
91. uzdisj
92. fseq1p1m1
93. fseq1m1p1
94. fz1sbc
95. elfzp1b
96. elfzm1b
97. elfzp12
98. fzm1
99. fzneuz
100. fznuz
101. uznfz
102. fzp1nel
103. fzrevral
104. fzrevral2
105. fzrevral3
106. fzshftral
107. ige2m1fz1
108. ige2m1fz
Finite intervals of nonnegative integers
1. elfz2nn0
2. fznn0
3. elfznn0
4. elfz3nn0
5. fz0ssnn0
6. fz1ssfz0
7. 0elfz
8. nn0fz0
9. elfz0add
10. fz0sn
11. fz0tp
12. fz0to3un2pr
13. fz0to4untppr
14. elfz0ubfz0
15. elfz0fzfz0
16. fz0fzelfz0
17. fznn0sub2
18. uzsubfz0
19. fz0fzdiffz0
20. elfzmlbm
21. elfzmlbp
22. fzctr
23. difelfzle
24. difelfznle
25. nn0split
26. nn0disj
27. fz0sn0fz1
28. fvffz0
29. 1fv
30. 4fvwrd4
31. 2ffzeq
32. preduz
33. prednn
34. prednn0
35. predfz
Half-open integer ranges
1. cfzo
2. df-fzo
3. fzof
4. elfzoel1
5. elfzoel2
6. elfzoelz
7. fzoval
8. elfzo
9. elfzo2
10. elfzouz
11. nelfzo
12. fzolb
13. fzolb2
14. elfzole1
15. elfzolt2
16. elfzolt3
17. elfzolt2b
18. elfzolt3b
19. fzonel
20. elfzouz2
21. elfzofz
22. elfzo3
23. fzon0
24. fzossfz
25. fzossz
26. fzon
27. fzo0n
28. fzonlt0
29. fzo0
30. fzonnsub
31. fzonnsub2
32. fzoss1
33. fzoss2
34. fzossrbm1
35. fzo0ss1
36. fzossnn0
37. fzospliti
38. fzosplit
39. fzodisj
40. fzouzsplit
41. fzouzdisj
42. fzoun
43. fzodisjsn
44. prinfzo0
45. lbfzo0
46. elfzo0
47. elfzo0z
48. nn0p1elfzo
49. elfzo0le
50. elfzonn0
51. fzonmapblen
52. fzofzim
53. fz1fzo0m1
54. fzossnn
55. elfzo1
56. fzo1fzo0n0
57. fzo0n0
58. fzoaddel
59. fzo0addel
60. fzo0addelr
61. fzoaddel2
62. elfzoext
63. elincfzoext
64. fzosubel
65. fzosubel2
66. fzosubel3
67. eluzgtdifelfzo
68. ige2m2fzo
69. fzocatel
70. ubmelfzo
71. elfzodifsumelfzo
72. elfzom1elp1fzo
73. elfzom1elfzo
74. fzval3
75. fz0add1fz1
76. fzosn
77. elfzomin
78. zpnn0elfzo
79. zpnn0elfzo1
80. fzosplitsnm1
81. elfzonlteqm1
82. fzonn0p1
83. fzossfzop1
84. fzonn0p1p1
85. elfzom1p1elfzo
86. fzo0ssnn0
87. fzo01
88. fzo12sn
89. fzo13pr
90. fzo0to2pr
91. fzo0to3tp
92. fzo0to42pr
93. fzo1to4tp
94. fzo0sn0fzo1
95. elfzo0l
96. fzoend
97. fzo0end
98. ssfzo12
99. ssfzoulel
100. ssfzo12bi
101. ubmelm1fzo
102. fzofzp1
103. fzofzp1b
104. elfzom1b
105. elfzom1elp1fzo1
106. elfzo1elm1fzo0
107. elfzonelfzo
108. fzonfzoufzol
109. elfzomelpfzo
110. elfznelfzo
111. elfznelfzob
112. peano2fzor
113. fzosplitsn
114. fzosplitpr
115. fzosplitprm1
116. fzosplitsni
117. fzisfzounsn
118. elfzr
119. elfzlmr
120. elfz0lmr
121. fzostep1
122. fzoshftral
123. fzind2
124. fvinim0ffz
125. injresinjlem
126. injresinj
127. subfzo0