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
163. nnge2recico01
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. elfzod
11. elfzouz
12. nelfzo
13. fzolb
14. fzolb2
15. elfzole1
16. elfzolt2
17. elfzolt3
18. elfzolt2b
19. elfzolt3b
20. elfzop1le2
21. fzonel
22. elfzouz2
23. elfzofz
24. elfzo3
25. fzon0
26. fzossfz
27. fzossz
28. fzon
29. fzo0n
30. fzonlt0
31. fzo0
32. fzonnsub
33. fzonnsub2
34. fzoss1
35. fzoss2
36. fzossrbm1
37. fzo0ss1
38. fzossnn0
39. fzospliti
40. fzosplit
41. fzodisj
42. fzouzsplit
43. fzouzdisj
44. fzoun
45. fzodisjsn
46. prinfzo0
47. lbfzo0
48. elfzo0
49. elfzo0z
50. nn0p1elfzo
51. elfzo0le
52. elfzolem1
53. elfzo0subge1
54. elfzo0suble
55. elfzonn0
56. fzonmapblen
57. fzofzim
58. fz1fzo0m1
59. fzossnn
60. elfzo1
61. fzo1lb
62. 1elfzo1
63. fzo1fzo0n0
64. fzo0n0
65. fzoaddel
66. fzo0addel
67. fzo0addelr
68. fzoaddel2
69. elfzoextl
70. elfzoext
71. elincfzoext
72. fzosubel
73. fzosubel2
74. fzosubel3
75. eluzgtdifelfzo
76. ige2m2fzo
77. fzocatel
78. ubmelfzo
79. elfzodifsumelfzo
80. elfzom1elp1fzo
81. elfzom1elfzo
82. fzval3
83. fz0add1fz1
84. fzosn
85. elfzomin
86. zpnn0elfzo
87. zpnn0elfzo1
88. fzosplitsnm1
89. elfzonlteqm1
90. fzonn0p1
91. fzossfzop1
92. fzonn0p1p1
93. elfzom1p1elfzo
94. fzo0ssnn0
95. fzo01
96. fzo12sn
97. fzo13pr
98. fzo0to2pr
99. fz01pr
100. fzo0to3tp
101. fzo0to42pr
102. fzo1to4tp
103. fzo0sn0fzo1
104. elfzo0l
105. fzoend
106. fzo0end
107. ssfzo12
108. ssfzoulel
109. ssfzo12bi
110. fzoopth
111. ubmelm1fzo
112. fzofzp1
113. fzofzp1b
114. elfzom1b
115. elfzom1elp1fzo1
116. elfzo1elm1fzo0
117. elfzonelfzo
118. elfzodif0
119. fzonfzoufzol
120. elfzomelpfzo
121. elfznelfzo
122. elfznelfzob
123. peano2fzor
124. fzosplitsn
125. fzosplitpr
126. fzosplitprm1
127. fzosplitsni
128. fzisfzounsn
129. elfzr
130. elfzlmr
131. elfz0lmr
132. fzone1
133. fzom1ne1
134. fzostep1
135. fzoshftral
136. fzind2
137. fvinim0ffz
138. injresinjlem
139. injresinj
140. subfzo0
141. fvf1tp