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. 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
  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. elicod
    51. icogelb
    52. elicore
    53. ubioc1
    54. lbico1
    55. iccleub
    56. iccgelb
    57. elioo5
    58. eliooxr
    59. eliooord
    60. elioo4g
    61. ioossre
    62. ioosscn
    63. elioc2
    64. elico2
    65. elicc2
    66. elicc2i
    67. elicc4
    68. iccss
    69. iccssioo
    70. icossico
    71. iccss2
    72. iccssico
    73. iccssioo2
    74. iccssico2
    75. ioomax
    76. iccmax
    77. ioopos
    78. ioorp
    79. iooshf
    80. iocssre
    81. icossre
    82. iccssre
    83. iccssxr
    84. iocssxr
    85. icossxr
    86. ioossicc
    87. iccssred
    88. eliccxr
    89. icossicc
    90. iocssicc
    91. ioossico
    92. iocssioo
    93. icossioo
    94. ioossioo
    95. iccsupr
    96. elioopnf
    97. elioomnf
    98. elicopnf
    99. repos
    100. ioof
    101. iccf
    102. unirnioo
    103. dfioo2
    104. ioorebas
    105. xrge0neqmnf
    106. xrge0nre
    107. elrege0
    108. nn0rp0
    109. rge0ssre
    110. elxrge0
    111. 0e0icopnf
    112. 0e0iccpnf
    113. ge0addcl
    114. ge0mulcl
    115. ge0xaddcl
    116. ge0xmulcl
    117. lbicc2
    118. ubicc2
    119. elicc01
    120. elunitrn
    121. elunitcn
    122. 0elunit
    123. 1elunit
    124. iooneg
    125. iccneg
    126. icoshft
    127. icoshftf1o
    128. icoun
    129. icodisj
    130. ioounsn
    131. snunioo
    132. snunico
    133. snunioc
    134. prunioo
    135. ioodisj
    136. ioojoin
    137. difreicc
    138. iccsplit
    139. iccshftr
    140. iccshftri
    141. iccshftl
    142. iccshftli
    143. iccdil
    144. iccdili
    145. icccntr
    146. icccntri
    147. divelunit
    148. lincmb01cmp
    149. iccf1o
    150. iccen
    151. xov1plusxeqvd
    152. unitssre
    153. unitsscn
    154. supicc
    155. supiccub
    156. supicclub
    157. supicclub2
    158. zltaddlt1le
    159. 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. 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