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. 5rp
9. rpssre
10. rpre
11. rpxr
12. rpcn
13. nnrp
14. rpgt0
15. rpge0
16. rpregt0
17. rprege0
18. rpne0
19. rprene0
20. rpcnne0
21. neglt
22. rpcndif0
23. ralrp
24. rexrp
25. rpaddcl
26. rpmulcl
27. rpmtmip
28. rpdivcl
29. rpreccl
30. rphalfcl
31. rpgecl
32. rphalflt
33. rerpdivcl
34. ge0p1rp
35. rpneg
36. negelrp
37. negelrpd
38. 0nrp
39. ltsubrp
40. ltaddrp
41. difrp
42. elrpd
43. nnrpd
44. zgt1rpn0n1
45. rpred
46. rpxrd
47. rpcnd
48. rpgt0d
49. rpge0d
50. rpne0d
51. rpregt0d
52. rprege0d
53. rprene0d
54. rpcnne0d
55. rpreccld
56. rprecred
57. rphalfcld
58. reclt1d
59. recgt1d
60. rpaddcld
61. rpmulcld
62. rpdivcld
63. ltrecd
64. lerecd
65. ltrec1d
66. lerec2d
67. lediv2ad
68. ltdiv2d
69. lediv2d
70. ledivdivd
71. divge1
72. divlt1lt
73. divle1le
74. ledivge1le
75. ge0p1rpd
76. rerpdivcld
77. ltsubrpd
78. ltaddrpd
79. ltaddrp2d
80. ltmulgt11d
81. ltmulgt12d
82. gt0divd
83. ge0divd
84. rpgecld
85. divge0d
86. ltmul1d
87. ltmul2d
88. lemul1d
89. lemul2d
90. ltdiv1d
91. lediv1d
92. ltmuldivd
93. ltmuldiv2d
94. lemuldivd
95. lemuldiv2d
96. ltdivmuld
97. ltdivmul2d
98. ledivmuld
99. ledivmul2d
100. ltmul1dd
101. ltmul2dd
102. ltdiv1dd
103. lediv1dd
104. lediv12ad
105. mul2lt0rlt0
106. mul2lt0rgt0
107. mul2lt0llt0
108. mul2lt0lgt0
109. mul2lt0bi
110. prodge0rd
111. prodge0ld
112. ltdiv23d
113. lediv23d
114. lt2mul2divd
115. nnledivrp
116. nn0ledivnn
117. addlelt
118. ge2halflem1
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. pnfged
24. xnn0n0n1ge2b
25. 0lepnf
26. xnn0ge0
27. mnfle
28. mnfled
29. xrltnsym
30. xrltnsym2
31. xrlttri
32. xrlttr
33. xrltso
34. xrlttri2
35. xrlttri3
36. xrleloe
37. xrleltne
38. xrltlen
39. dfle2
40. dflt2
41. xrltle
42. xrltled
43. xrleid
44. xrleidd
45. xrletri
46. xrletri3
47. xrletrid
48. xrlelttr
49. xrltletr
50. xrletr
51. xrlttrd
52. xrlelttrd
53. xrltletrd
54. xrletrd
55. xrltne
56. xrgtned
57. nltpnft
58. xgepnf
59. ngtmnft
60. xlemnf
61. xrrebnd
62. xrre
63. xrre2
64. xrre3
65. ge0gtmnf
66. ge0nemnf
67. xrrege0
68. xrmax1
69. xrmax2
70. xrmin1
71. xrmin2
72. xrmaxeq
73. xrmineq
74. xrmaxlt
75. xrltmin
76. xrmaxle
77. xrlemin
78. max1
79. max1ALT
80. max2
81. 2resupmax
82. min1
83. min2
84. maxle
85. lemin
86. maxlt
87. ltmin
88. lemaxle
89. max0sub
90. ifle
91. z2ge
92. qbtwnre
93. qbtwnxr
94. qsqueeze
95. qextltlem
96. qextlt
97. qextle
98. xralrple
99. alrple
100. xnegeq
101. xnegex
102. xnegpnf
103. xnegmnf
104. rexneg
105. xneg0
106. xnegcl
107. xnegneg
108. xneg11
109. xltnegi
110. xltneg
111. xleneg
112. xlt0neg1
113. xlt0neg2
114. xle0neg1
115. xle0neg2
116. xaddval
117. xaddf
118. xmulval
119. xaddpnf1
120. xaddpnf2
121. xaddmnf1
122. xaddmnf2
123. pnfaddmnf
124. mnfaddpnf
125. rexadd
126. rexsub
127. rexaddd
128. xnn0xaddcl
129. xaddnemnf
130. xaddnepnf
131. xnegid
132. xaddcl
133. xaddcom
134. xaddrid
135. xaddlid
136. xaddridd
137. xnn0lem1lt
138. xnn0lenn0nn0
139. xnn0le2is012
140. xnn0xadd0
141. xnegdi
142. xaddass
143. xaddass2
144. xpncan
145. xnpcan
146. xleadd1a
147. xleadd2a
148. xleadd1
149. xltadd1
150. xltadd2
151. xaddge0
152. xle2add
153. xlt2add
154. xsubge0
155. xposdif
156. xlesubadd
157. xmullem
158. xmullem2
159. xmulcom
160. xmul01
161. xmul02
162. xmulneg1
163. xmulneg2
164. rexmul
165. xmulf
166. xmulcl
167. xmulpnf1
168. xmulpnf2
169. xmulmnf1
170. xmulmnf2
171. xmulpnf1n
172. xmulrid
173. xmullid
174. xmulm1
175. xmulasslem2
176. xmulgt0
177. xmulge0
178. xmulasslem
179. xmulasslem3
180. xmulass
181. xlemul1a
182. xlemul2a
183. xlemul1
184. xlemul2
185. xltmul1
186. xltmul2
187. xadddilem
188. xadddi
189. xadddir
190. xadddi2
191. xadddi2r
192. x2times
193. xnegcld
194. xaddcld
195. xmulcld
196. xadd4d
197. 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. xrsupssd
30. infxrcl
31. infxrlb
32. infxrgelb
33. infxrre
34. infxrmnf
35. xrinf0
36. infxrss
37. reltre
38. rpltrp
39. reltxrnmnf
40. infmremnf
41. 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. icogelbd
54. elicore
55. ubioc1
56. lbico1
57. iccleub
58. iccgelb
59. elioo5
60. eliooxr
61. eliooord
62. elioo4g
63. ioossre
64. ioosscn
65. elioc2
66. elico2
67. elicc2
68. elicc2i
69. elicc4
70. iccss
71. iccssioo
72. icossico
73. iccss2
74. iccssico
75. iccssioo2
76. iccssico2
77. icossico2d
78. ioomax
79. iccmax
80. ioopos
81. ioorp
82. iooshf
83. iocssre
84. icossre
85. iccssre
86. iccssxr
87. iocssxr
88. icossxr
89. ioossicc
90. iccssred
91. eliccxr
92. icossicc
93. iocssicc
94. ioossico
95. iocssioo
96. icossioo
97. ioossioo
98. iccsupr
99. elioopnf
100. elioomnf
101. elicopnf
102. repos
103. ioof
104. iccf
105. unirnioo
106. dfioo2
107. ioorebas
108. xrge0neqmnf
109. xrge0nre
110. elrege0
111. nn0rp0
112. rge0ssre
113. elxrge0
114. 0e0icopnf
115. 0e0iccpnf
116. ge0addcl
117. ge0mulcl
118. ge0xaddcl
119. ge0xmulcl
120. lbicc2
121. ubicc2
122. elicc01
123. elunitrn
124. elunitcn
125. 0elunit
126. 1elunit
127. iooneg
128. iccneg
129. icoshft
130. icoshftf1o
131. icoun
132. icodisj
133. ioounsn
134. snunioo
135. snunico
136. snunioc
137. prunioo
138. ioodisj
139. ioojoin
140. difreicc
141. iccsplit
142. iccshftr
143. iccshftri
144. iccshftl
145. iccshftli
146. iccdil
147. iccdili
148. icccntr
149. icccntri
150. divelunit
151. lincmb01cmp
152. iccf1o
153. iccen
154. xov1plusxeqvd
155. unitssre
156. unitsscn
157. supicc
158. supiccub
159. supicclub
160. supicclub2
161. zltaddlt1le
162. 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. fzne1
99. fzdif1
100. fz0dif1
101. fzm1
102. fzneuz
103. fznuz
104. uznfz
105. fzp1nel
106. fzrevral
107. fzrevral2
108. fzrevral3
109. fzshftral
110. ige2m1fz1
111. 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. fz0to5un2tp
15. elfz0ubfz0
16. elfz0fzfz0
17. fz0fzelfz0
18. fznn0sub2
19. uzsubfz0
20. fz0fzdiffz0
21. elfzmlbm
22. elfzmlbp
23. fzctr
24. difelfzle
25. difelfznle
26. nn0split
27. nn0disj
28. fz0sn0fz1
29. fvffz0
30. 1fv
31. 4fvwrd4
32. 2ffzeq
33. preduz
34. prednn
35. prednn0
36. 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. elfzop1le2
20. fzonel
21. elfzouz2
22. elfzofz
23. elfzo3
24. fzon0
25. fzossfz
26. fzossz
27. fzon
28. fzo0n
29. fzonlt0
30. fzo0
31. fzonnsub
32. fzonnsub2
33. fzoss1
34. fzoss2
35. fzossrbm1
36. fzo0ss1
37. fzossnn0
38. fzospliti
39. fzosplit
40. fzodisj
41. fzouzsplit
42. fzouzdisj
43. fzoun
44. fzodisjsn
45. prinfzo0
46. lbfzo0
47. elfzo0
48. elfzo0z
49. nn0p1elfzo
50. elfzo0le
51. elfzolem1
52. elfzo0subge1
53. elfzo0suble
54. elfzonn0
55. fzonmapblen
56. fzofzim
57. fz1fzo0m1
58. fzossnn
59. elfzo1
60. fzo1lb
61. 1elfzo1
62. fzo1fzo0n0
63. fzo0n0
64. fzoaddel
65. fzo0addel
66. fzo0addelr
67. fzoaddel2
68. elfzoextl
69. elfzoext
70. elincfzoext
71. fzosubel
72. fzosubel2
73. fzosubel3
74. eluzgtdifelfzo
75. ige2m2fzo
76. fzocatel
77. ubmelfzo
78. elfzodifsumelfzo
79. elfzom1elp1fzo
80. elfzom1elfzo
81. fzval3
82. fz0add1fz1
83. fzosn
84. elfzomin
85. zpnn0elfzo
86. zpnn0elfzo1
87. fzosplitsnm1
88. elfzonlteqm1
89. fzonn0p1
90. fzossfzop1
91. fzonn0p1p1
92. elfzom1p1elfzo
93. fzo0ssnn0
94. fzo01
95. fzo12sn
96. fzo13pr
97. fzo0to2pr
98. fz01pr
99. fzo0to3tp
100. fzo0to42pr
101. fzo1to4tp
102. fzo0sn0fzo1
103. elfzo0l
104. fzoend
105. fzo0end
106. ssfzo12
107. ssfzoulel
108. ssfzo12bi
109. fzoopth
110. ubmelm1fzo
111. fzofzp1
112. fzofzp1b
113. elfzom1b
114. elfzom1elp1fzo1
115. elfzo1elm1fzo0
116. elfzonelfzo
117. elfzodif0
118. fzonfzoufzol
119. elfzomelpfzo
120. elfznelfzo
121. elfznelfzob
122. peano2fzor
123. fzosplitsn
124. fzosplitpr
125. fzosplitprm1
126. fzosplitsni
127. fzisfzounsn
128. elfzr
129. elfzlmr
130. elfz0lmr
131. fzone1
132. fzom1ne1
133. fzostep1
134. fzoshftral
135. fzind2
136. fvinim0ffz
137. injresinjlem
138. injresinj
139. subfzo0
140. fvf1tp