Metamath Proof Explorer


Table of Contents - 5.5. Order sets

  1. 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
  2. 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. mnfled
    28. xrltnsym
    29. xrltnsym2
    30. xrlttri
    31. xrlttr
    32. xrltso
    33. xrlttri2
    34. xrlttri3
    35. xrleloe
    36. xrleltne
    37. xrltlen
    38. dfle2
    39. dflt2
    40. xrltle
    41. xrltled
    42. xrleid
    43. xrleidd
    44. xrletri
    45. xrletri3
    46. xrletrid
    47. xrlelttr
    48. xrltletr
    49. xrletr
    50. xrlttrd
    51. xrlelttrd
    52. xrltletrd
    53. xrletrd
    54. xrltne
    55. nltpnft
    56. xgepnf
    57. ngtmnft
    58. xlemnf
    59. xrrebnd
    60. xrre
    61. xrre2
    62. xrre3
    63. ge0gtmnf
    64. ge0nemnf
    65. xrrege0
    66. xrmax1
    67. xrmax2
    68. xrmin1
    69. xrmin2
    70. xrmaxeq
    71. xrmineq
    72. xrmaxlt
    73. xrltmin
    74. xrmaxle
    75. xrlemin
    76. max1
    77. max1ALT
    78. max2
    79. 2resupmax
    80. min1
    81. min2
    82. maxle
    83. lemin
    84. maxlt
    85. ltmin
    86. lemaxle
    87. max0sub
    88. ifle
    89. z2ge
    90. qbtwnre
    91. qbtwnxr
    92. qsqueeze
    93. qextltlem
    94. qextlt
    95. qextle
    96. xralrple
    97. alrple
    98. xnegeq
    99. xnegex
    100. xnegpnf
    101. xnegmnf
    102. rexneg
    103. xneg0
    104. xnegcl
    105. xnegneg
    106. xneg11
    107. xltnegi
    108. xltneg
    109. xleneg
    110. xlt0neg1
    111. xlt0neg2
    112. xle0neg1
    113. xle0neg2
    114. xaddval
    115. xaddf
    116. xmulval
    117. xaddpnf1
    118. xaddpnf2
    119. xaddmnf1
    120. xaddmnf2
    121. pnfaddmnf
    122. mnfaddpnf
    123. rexadd
    124. rexsub
    125. rexaddd
    126. xnn0xaddcl
    127. xaddnemnf
    128. xaddnepnf
    129. xnegid
    130. xaddcl
    131. xaddcom
    132. xaddrid
    133. xaddlid
    134. xaddridd
    135. xnn0lem1lt
    136. xnn0lenn0nn0
    137. xnn0le2is012
    138. xnn0xadd0
    139. xnegdi
    140. xaddass
    141. xaddass2
    142. xpncan
    143. xnpcan
    144. xleadd1a
    145. xleadd2a
    146. xleadd1
    147. xltadd1
    148. xltadd2
    149. xaddge0
    150. xle2add
    151. xlt2add
    152. xsubge0
    153. xposdif
    154. xlesubadd
    155. xmullem
    156. xmullem2
    157. xmulcom
    158. xmul01
    159. xmul02
    160. xmulneg1
    161. xmulneg2
    162. rexmul
    163. xmulf
    164. xmulcl
    165. xmulpnf1
    166. xmulpnf2
    167. xmulmnf1
    168. xmulmnf2
    169. xmulpnf1n
    170. xmulrid
    171. xmullid
    172. xmulm1
    173. xmulasslem2
    174. xmulgt0
    175. xmulge0
    176. xmulasslem
    177. xmulasslem3
    178. xmulass
    179. xlemul1a
    180. xlemul2a
    181. xlemul1
    182. xlemul2
    183. xltmul1
    184. xltmul2
    185. xadddilem
    186. xadddi
    187. xadddir
    188. xadddi2
    189. xadddi2r
    190. x2times
    191. xnegcld
    192. xaddcld
    193. xmulcld
    194. xadd4d
    195. xnn0add4d
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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. elfzonn0
    52. fzonmapblen
    53. fzofzim
    54. fz1fzo0m1
    55. fzossnn
    56. elfzo1
    57. fzo1fzo0n0
    58. fzo0n0
    59. fzoaddel
    60. fzo0addel
    61. fzo0addelr
    62. fzoaddel2
    63. elfzoext
    64. elincfzoext
    65. fzosubel
    66. fzosubel2
    67. fzosubel3
    68. eluzgtdifelfzo
    69. ige2m2fzo
    70. fzocatel
    71. ubmelfzo
    72. elfzodifsumelfzo
    73. elfzom1elp1fzo
    74. elfzom1elfzo
    75. fzval3
    76. fz0add1fz1
    77. fzosn
    78. elfzomin
    79. zpnn0elfzo
    80. zpnn0elfzo1
    81. fzosplitsnm1
    82. elfzonlteqm1
    83. fzonn0p1
    84. fzossfzop1
    85. fzonn0p1p1
    86. elfzom1p1elfzo
    87. fzo0ssnn0
    88. fzo01
    89. fzo12sn
    90. fzo13pr
    91. fzo0to2pr
    92. fzo0to3tp
    93. fzo0to42pr
    94. fzo1to4tp
    95. fzo0sn0fzo1
    96. elfzo0l
    97. fzoend
    98. fzo0end
    99. ssfzo12
    100. ssfzoulel
    101. ssfzo12bi
    102. ubmelm1fzo
    103. fzofzp1
    104. fzofzp1b
    105. elfzom1b
    106. elfzom1elp1fzo1
    107. elfzo1elm1fzo0
    108. elfzonelfzo
    109. fzonfzoufzol
    110. elfzomelpfzo
    111. elfznelfzo
    112. elfznelfzob
    113. peano2fzor
    114. fzosplitsn
    115. fzosplitpr
    116. fzosplitprm1
    117. fzosplitsni
    118. fzisfzounsn
    119. elfzr
    120. elfzlmr
    121. elfz0lmr
    122. fzostep1
    123. fzoshftral
    124. fzind2
    125. fvinim0ffz
    126. injresinjlem
    127. injresinj
    128. subfzo0