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. nltpnft
57. xgepnf
58. ngtmnft
59. xlemnf
60. xrrebnd
61. xrre
62. xrre2
63. xrre3
64. ge0gtmnf
65. ge0nemnf
66. xrrege0
67. xrmax1
68. xrmax2
69. xrmin1
70. xrmin2
71. xrmaxeq
72. xrmineq
73. xrmaxlt
74. xrltmin
75. xrmaxle
76. xrlemin
77. max1
78. max1ALT
79. max2
80. 2resupmax
81. min1
82. min2
83. maxle
84. lemin
85. maxlt
86. ltmin
87. lemaxle
88. max0sub
89. ifle
90. z2ge
91. qbtwnre
92. qbtwnxr
93. qsqueeze
94. qextltlem
95. qextlt
96. qextle
97. xralrple
98. alrple
99. xnegeq
100. xnegex
101. xnegpnf
102. xnegmnf
103. rexneg
104. xneg0
105. xnegcl
106. xnegneg
107. xneg11
108. xltnegi
109. xltneg
110. xleneg
111. xlt0neg1
112. xlt0neg2
113. xle0neg1
114. xle0neg2
115. xaddval
116. xaddf
117. xmulval
118. xaddpnf1
119. xaddpnf2
120. xaddmnf1
121. xaddmnf2
122. pnfaddmnf
123. mnfaddpnf
124. rexadd
125. rexsub
126. rexaddd
127. xnn0xaddcl
128. xaddnemnf
129. xaddnepnf
130. xnegid
131. xaddcl
132. xaddcom
133. xaddrid
134. xaddlid
135. xaddridd
136. xnn0lem1lt
137. xnn0lenn0nn0
138. xnn0le2is012
139. xnn0xadd0
140. xnegdi
141. xaddass
142. xaddass2
143. xpncan
144. xnpcan
145. xleadd1a
146. xleadd2a
147. xleadd1
148. xltadd1
149. xltadd2
150. xaddge0
151. xle2add
152. xlt2add
153. xsubge0
154. xposdif
155. xlesubadd
156. xmullem
157. xmullem2
158. xmulcom
159. xmul01
160. xmul02
161. xmulneg1
162. xmulneg2
163. rexmul
164. xmulf
165. xmulcl
166. xmulpnf1
167. xmulpnf2
168. xmulmnf1
169. xmulmnf2
170. xmulpnf1n
171. xmulrid
172. xmullid
173. xmulm1
174. xmulasslem2
175. xmulgt0
176. xmulge0
177. xmulasslem
178. xmulasslem3
179. xmulass
180. xlemul1a
181. xlemul2a
182. xlemul1
183. xlemul2
184. xltmul1
185. xltmul2
186. xadddilem
187. xadddi
188. xadddir
189. xadddi2
190. xadddi2r
191. x2times
192. xnegcld
193. xaddcld
194. xmulcld
195. xadd4d
196. 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. fzonfzoufzol
118. elfzomelpfzo
119. elfznelfzo
120. elfznelfzob
121. peano2fzor
122. fzosplitsn
123. fzosplitpr
124. fzosplitprm1
125. fzosplitsni
126. fzisfzounsn
127. elfzr
128. elfzlmr
129. elfz0lmr
130. fzostep1
131. fzoshftral
132. fzind2
133. fvinim0ffz
134. injresinjlem
135. injresinj
136. subfzo0
137. fvf1tp