Metamath Proof Explorer

Table of Contents - 5.3.4. Ordering on reals (cont.)

  1. gt0ne0
  2. lt0ne0
  3. ltadd1
  4. leadd1
  5. leadd2
  6. ltsubadd
  7. ltsubadd2
  8. lesubadd
  9. lesubadd2
  10. ltaddsub
  11. ltaddsub2
  12. leaddsub
  13. leaddsub2
  14. suble
  15. lesub
  16. ltsub23
  17. ltsub13
  18. le2add
  19. ltleadd
  20. leltadd
  21. lt2add
  22. addgt0
  23. addgegt0
  24. addgtge0
  25. addge0
  26. ltaddpos
  27. ltaddpos2
  28. ltsubpos
  29. posdif
  30. lesub1
  31. lesub2
  32. ltsub1
  33. ltsub2
  34. lt2sub
  35. le2sub
  36. ltneg
  37. ltnegcon1
  38. ltnegcon2
  39. leneg
  40. lenegcon1
  41. lenegcon2
  42. lt0neg1
  43. lt0neg2
  44. le0neg1
  45. le0neg2
  46. addge01
  47. addge02
  48. add20
  49. subge0
  50. suble0
  51. leaddle0
  52. subge02
  53. lesub0
  54. mulge0
  55. mullt0
  56. msqgt0
  57. msqge0
  58. 0lt1
  59. 0le1
  60. relin01
  61. ltordlem
  62. ltord1
  63. leord1
  64. eqord1
  65. ltord2
  66. leord2
  67. eqord2
  68. wloglei
  69. wlogle
  70. leidi
  71. gt0ne0i
  72. gt0ne0ii
  73. msqgt0i
  74. msqge0i
  75. addgt0i
  76. addge0i
  77. addgegt0i
  78. addgt0ii
  79. add20i
  80. ltnegi
  81. lenegi
  82. ltnegcon2i
  83. mulge0i
  84. lesub0i
  85. ltaddposi
  86. posdifi
  87. ltnegcon1i
  88. lenegcon1i
  89. subge0i
  90. ltadd1i
  91. leadd1i
  92. leadd2i
  93. ltsubaddi
  94. lesubaddi
  95. ltsubadd2i
  96. lesubadd2i
  97. ltaddsubi
  98. lt2addi
  99. le2addi
  100. gt0ne0d
  101. lt0ne0d
  102. leidd
  103. msqgt0d
  104. msqge0d
  105. lt0neg1d
  106. lt0neg2d
  107. le0neg1d
  108. le0neg2d
  109. addgegt0d
  110. addgtge0d
  111. addgt0d
  112. addge0d
  113. mulge0d
  114. ltnegd
  115. lenegd
  116. ltnegcon1d
  117. ltnegcon2d
  118. lenegcon1d
  119. lenegcon2d
  120. ltaddposd
  121. ltaddpos2d
  122. ltsubposd
  123. posdifd
  124. addge01d
  125. addge02d
  126. subge0d
  127. suble0d
  128. subge02d
  129. ltadd1d
  130. leadd1d
  131. leadd2d
  132. ltsubaddd
  133. lesubaddd
  134. ltsubadd2d
  135. lesubadd2d
  136. ltaddsubd
  137. ltaddsub2d
  138. leaddsub2d
  139. subled
  140. lesubd
  141. ltsub23d
  142. ltsub13d
  143. lesub1d
  144. lesub2d
  145. ltsub1d
  146. ltsub2d
  147. ltadd1dd
  148. ltsub1dd
  149. ltsub2dd
  150. leadd1dd
  151. leadd2dd
  152. lesub1dd
  153. lesub2dd
  154. lesub3d
  155. le2addd
  156. le2subd
  157. ltleaddd
  158. leltaddd
  159. lt2addd
  160. lt2subd
  161. possumd
  162. sublt0d
  163. ltaddsublt
  164. 1le1