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. elicod
51. icogelb
52. elicore
53. ubioc1
54. lbico1
55. iccleub
56. iccgelb
57. elioo5
58. eliooxr
59. eliooord
60. elioo4g
61. ioossre
62. elioc2
63. elico2
64. elicc2
65. elicc2i
66. elicc4
67. iccss
68. iccssioo
69. icossico
70. iccss2
71. iccssico
72. iccssioo2
73. iccssico2
74. ioomax
75. iccmax
76. ioopos
77. ioorp
78. iooshf
79. iocssre
80. icossre
81. iccssre
82. iccssxr
83. iocssxr
84. icossxr
85. ioossicc
86. eliccxr
87. icossicc
88. iocssicc
89. ioossico
90. iocssioo
91. icossioo
92. ioossioo
93. iccsupr
94. elioopnf
95. elioomnf
96. elicopnf
97. repos
98. ioof
99. iccf
100. unirnioo
101. dfioo2
102. ioorebas
103. xrge0neqmnf
104. xrge0nre
105. elrege0
106. nn0rp0
107. rge0ssre
108. elxrge0
109. 0e0icopnf
110. 0e0iccpnf
111. ge0addcl
112. ge0mulcl
113. ge0xaddcl
114. ge0xmulcl
115. lbicc2
116. ubicc2
117. elicc01
118. elunitrn
119. elunitcn
120. 0elunit
121. 1elunit
122. iooneg
123. iccneg
124. icoshft
125. icoshftf1o
126. icoun
127. icodisj
128. ioounsn
129. snunioo
130. snunico
131. snunioc
132. prunioo
133. ioodisj
134. ioojoin
135. difreicc
136. iccsplit
137. iccshftr
138. iccshftri
139. iccshftl
140. iccshftli
141. iccdil
142. iccdili
143. icccntr
144. icccntri
145. divelunit
146. lincmb01cmp
147. iccf1o
148. iccen
149. xov1plusxeqvd
150. unitssre
151. unitsscn
152. supicc
153. supiccub
154. supicclub
155. supicclub2
156. zltaddlt1le
157. xnn0xrge0
Finite intervals of integers
1. cfz
2. df-fz
3. fzval
4. fzval2
5. fzf
6. elfz1
7. elfz
8. elfz2
9. elfz5
10. elfz4
11. elfzuzb
12. eluzfz
13. elfzuz
14. elfzuz3
15. elfzel2
16. elfzel1
17. elfzelz
18. fzssz
19. elfzle1
20. elfzle2
21. elfzuz2
22. elfzle3
23. eluzfz1
24. eluzfz2
25. eluzfz2b
26. elfz3
27. elfz1eq
28. elfzubelfz
29. peano2fzr
30. fzn0
31. fz0
32. fzn
33. fzen
34. fz1n
35. 0nelfz1
36. 0fz1
37. fz10
38. uzsubsubfz
39. uzsubsubfz1
40. ige3m2fz
41. fzsplit2
42. fzsplit
43. fzdisj
44. fz01en
45. elfznn
46. elfz1end
47. fz1ssnn
48. fznn0sub
49. fzmmmeqm
50. fzaddel
51. fzadd2
52. fzsubel
53. fzopth
54. fzass4
55. fzss1
56. fzss2
57. fzssuz
58. fzsn
59. fzssp1
60. fzssnn
61. ssfzunsnext
62. ssfzunsn
63. fzsuc
64. fzpred
65. fzpreddisj
66. elfzp1
67. fzp1ss
68. fzelp1
69. fzp1elp1
70. fznatpl1
71. fzpr
72. fztp
73. fz12pr
74. fzsuc2
75. fzp1disj
76. fzdifsuc
77. fzprval
78. fztpval
79. fzrev
80. fzrev2
81. fzrev2i
82. fzrev3
83. fzrev3i
84. fznn
85. elfz1b
86. elfz1uz
87. elfzm11
88. uzsplit
89. uzdisj
90. fseq1p1m1
91. fseq1m1p1
92. fz1sbc
93. elfzp1b
94. elfzm1b
95. elfzp12
96. fzm1
97. fzneuz
98. fznuz
99. uznfz
100. fzp1nel
101. fzrevral
102. fzrevral2
103. fzrevral3
104. fzshftral
105. ige2m1fz1
106. 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