Home | Metamath
Proof Explorer Theorem List (p. 102 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lerelxr 10101 | 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
Theorem | lerel 10102 | 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | xrlenlt 10103 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.) |
Theorem | xrlenltd 10104 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Theorem | xrltnle 10105 | 'Less than' expressed in terms of 'less than or equal to', for extended reals. (Contributed by NM, 6-Feb-2007.) |
Theorem | xrnltled 10106 | 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | ssxr 10107 | The three (non-exclusive) possibilities implied by a subset of extended reals. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | ltxrlt 10108 | The standard less-than and the extended real less-than are identical when restricted to the non-extended reals . (Contributed by NM, 13-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | axlttri 10109 | Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-lttri 10010 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axlttrn 10110 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 10011 with ordering on the extended reals. New proofs should use lttr 10114 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axltadd 10111 | Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-ltadd 10012 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axmulgt0 10112 | The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-mulgt0 10013 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axsup 10113* | A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-sup 10014 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
Theorem | lttr 10114 | Alias for axlttrn 10110, for naming consistency with lttri 10163. New proofs should generally use this instead of ax-pre-lttrn 10011. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulgt0 10115 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
Theorem | lenlt 10116 | 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.) |
Theorem | ltnle 10117 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
Theorem | ltso 10118 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
Theorem | gtso 10119 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
Theorem | lttri2 10120 | Consequence of trichotomy. (Contributed by NM, 9-Oct-1999.) |
Theorem | lttri3 10121 | Trichotomy law for 'less than'. (Contributed by NM, 5-May-1999.) |
Theorem | lttri4 10122 | Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | letri3 10123 | Trichotomy law. (Contributed by NM, 14-May-1999.) |
Theorem | leloe 10124 | 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.) |
Theorem | eqlelt 10125 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
Theorem | ltle 10126 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.) |
Theorem | leltne 10127 | 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999.) |
Theorem | lelttr 10128 | Transitive law. (Contributed by NM, 23-May-1999.) |
Theorem | ltletr 10129 | Transitive law. (Contributed by NM, 25-Aug-1999.) |
Theorem | ltleletr 10130 | Transitive law, weaker form of ltletr 10129. (Contributed by AV, 14-Oct-2018.) |
Theorem | letr 10131 | Transitive law. (Contributed by NM, 12-Nov-1999.) |
Theorem | ltnr 10132 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | leid 10133 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | ltne 10134 | 'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.) |
Theorem | ltnsym 10135 | 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.) |
Theorem | ltnsym2 10136 | 'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | letric 10137 | Trichotomy law. (Contributed by NM, 18-Aug-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | ltlen 10138 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.) |
Theorem | eqle 10139 | Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.) |
Theorem | eqled 10140 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | ltadd2 10141 | Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | ne0gt0 10142 | A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007.) |
Theorem | lecasei 10143 | Ordering elimination by cases. (Contributed by NM, 6-Jul-2007.) |
Theorem | lelttric 10144 | Trichotomy law. (Contributed by NM, 4-Apr-2005.) |
Theorem | ltlecasei 10145 | Ordering elimination by cases. (Contributed by NM, 1-Jul-2007.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | ltnri 10146 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | eqlei 10147 | Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.) |
Theorem | eqlei2 10148 | Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
Theorem | gtneii 10149 | 'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.) |
Theorem | ltneii 10150 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.) |
Theorem | lttri2i 10151 | Consequence of trichotomy. (Contributed by NM, 19-Jan-1997.) |
Theorem | lttri3i 10152 | Consequence of trichotomy. (Contributed by NM, 14-May-1999.) |
Theorem | letri3i 10153 | Consequence of trichotomy. (Contributed by NM, 14-May-1999.) |
Theorem | leloei 10154 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 14-May-1999.) |
Theorem | ltleni 10155 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.) |
Theorem | ltnsymi 10156 | 'Less than' is not symmetric. (Contributed by NM, 6-May-1999.) |
Theorem | lenlti 10157 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.) |
Theorem | ltnlei 10158 | 'Less than' in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
Theorem | ltlei 10159 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.) |
Theorem | ltleii 10160 | 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.) |
Theorem | ltnei 10161 | 'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.) |
Theorem | letrii 10162 | Trichotomy law for 'less than or equal to'. (Contributed by NM, 2-Aug-1999.) |
Theorem | lttri 10163 | 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
Theorem | lelttri 10164 | 'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.) |
Theorem | ltletri 10165 | 'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.) |
Theorem | letri 10166 | 'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.) |
Theorem | le2tri3i 10167 | Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.) |
Theorem | ltadd2i 10168 | Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.) (Proof shortened by OpenAI, 25-Mar-2020.) |
Theorem | mulgt0i 10169 | The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
Theorem | mulgt0ii 10170 | The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
Theorem | ltnrd 10171 | 'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | gtned 10172 | 'Less than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltned 10173 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ne0gt0d 10174 | A nonzero nonnegative number is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lttrid 10175 | Ordering on reals satisfies strict trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lttri2d 10176 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lttri3d 10177 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lttri4d 10178 | Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | letri3d 10179 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | leloed 10180 | 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | eqleltd 10181 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
Theorem | ltlend 10182 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lenltd 10183 | 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltnled 10184 | 'Less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltled 10185 | 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltnsymd 10186 | 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | nltled 10187 | 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | lensymd 10188 | 'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | letrid 10189 | Trichotomy law for 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | leltned 10190 | 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | leneltd 10191 | 'Less than or equal to' and 'not equals' implies 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | mulgt0d 10192 | The product of two positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltadd2d 10193 | Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | letrd 10194 | Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.) |
Theorem | lelttrd 10195 | Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.) |
Theorem | ltadd2dd 10196 | Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.) |
Theorem | ltletrd 10197 | Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.) |
Theorem | lttrd 10198 | Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.) |
Theorem | lelttrdi 10199 | If a number is less than another number, and the other number is less than or equal to a third number, the first number is less than the third number. (Contributed by Alexander van der Vekens, 24-Mar-2018.) |
Theorem | dedekind 10200* | The Dedekind cut theorem. This theorem, which may be used to replace ax-pre-sup 10014 with appropriate adjustments, states that, if completely preceeds , then there is some number separating the two of them. (Contributed by Scott Fenton, 13-Jun-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |