![]() |
Metamath
Proof Explorer Theorem List (p. 114 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrlenlt 11301 | "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด โค ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | xrlenltd 11302 | "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) โ โข (๐ โ (๐ด โค ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | xrltnle 11303 | "Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ ยฌ ๐ต โค ๐ด)) | ||
Theorem | xrnltled 11304 | "Not less than" implies "less than or equal to". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ยฌ ๐ต < ๐ด) โ โข (๐ โ ๐ด โค ๐ต) | ||
Theorem | ssxr 11305 | 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 11306 | 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 11307 | 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 11204 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต < ๐ด))) | ||
Theorem | axlttrn 11308 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 11205 with ordering on the extended reals. New proofs should use lttr 11312 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | axltadd 11309 | 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 11206 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < ๐ต โ (๐ถ + ๐ด) < (๐ถ + ๐ต))) | ||
Theorem | axmulgt0 11310 | 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 11207 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 < ๐ด โง 0 < ๐ต) โ 0 < (๐ด ยท ๐ต))) | ||
Theorem | axsup 11311* | 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 11208 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
โข ((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ < ๐ฅ) โ โ๐ฅ โ โ (โ๐ฆ โ ๐ด ยฌ ๐ฅ < ๐ฆ โง โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ง โ ๐ด ๐ฆ < ๐ง))) | ||
Theorem | lttr 11312 | Alias for axlttrn 11308, for naming consistency with lttri 11362. New proofs should generally use this instead of ax-pre-lttrn 11205. (Contributed by NM, 10-Mar-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | mulgt0 11313 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 < (๐ด ยท ๐ต)) | ||
Theorem | lenlt 11314 | 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | ltnle 11315 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ยฌ ๐ต โค ๐ด)) | ||
Theorem | ltso 11316 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
โข < Or โ | ||
Theorem | gtso 11317 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
โข โก < Or โ | ||
Theorem | lttri2 11318 | Consequence of trichotomy. (Contributed by NM, 9-Oct-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โ ๐ต โ (๐ด < ๐ต โจ ๐ต < ๐ด))) | ||
Theorem | lttri3 11319 | Trichotomy law for 'less than'. (Contributed by NM, 5-May-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด = ๐ต โ (ยฌ ๐ด < ๐ต โง ยฌ ๐ต < ๐ด))) | ||
Theorem | lttri4 11320 | Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โจ ๐ด = ๐ต โจ ๐ต < ๐ด)) | ||
Theorem | letri3 11321 | Trichotomy law. (Contributed by NM, 14-May-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด = ๐ต โ (๐ด โค ๐ต โง ๐ต โค ๐ด))) | ||
Theorem | leloe 11322 | 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โ (๐ด < ๐ต โจ ๐ด = ๐ต))) | ||
Theorem | eqlelt 11323 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด = ๐ต โ (๐ด โค ๐ต โง ยฌ ๐ด < ๐ต))) | ||
Theorem | ltle 11324 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ๐ด โค ๐ต)) | ||
Theorem | leltne 11325 | 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด โค ๐ต) โ (๐ด < ๐ต โ ๐ต โ ๐ด)) | ||
Theorem | lelttr 11326 | Transitive law. (Contributed by NM, 23-May-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โค ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | leltletr 11327 | Transitive law, weaker form of lelttr 11326. (Contributed by AV, 14-Oct-2018.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โค ๐ต โง ๐ต < ๐ถ) โ ๐ด โค ๐ถ)) | ||
Theorem | ltletr 11328 | Transitive law. (Contributed by NM, 25-Aug-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ต โง ๐ต โค ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | ltleletr 11329 | Transitive law, weaker form of ltletr 11328. (Contributed by AV, 14-Oct-2018.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ต โง ๐ต โค ๐ถ) โ ๐ด โค ๐ถ)) | ||
Theorem | letr 11330 | Transitive law. (Contributed by NM, 12-Nov-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โค ๐ต โง ๐ต โค ๐ถ) โ ๐ด โค ๐ถ)) | ||
Theorem | ltnr 11331 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
โข (๐ด โ โ โ ยฌ ๐ด < ๐ด) | ||
Theorem | leid 11332 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
โข (๐ด โ โ โ ๐ด โค ๐ด) | ||
Theorem | ltne 11333 | 'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.) |
โข ((๐ด โ โ โง ๐ด < ๐ต) โ ๐ต โ ๐ด) | ||
Theorem | ltnsym 11334 | 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | ltnsym2 11335 | 'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ยฌ (๐ด < ๐ต โง ๐ต < ๐ด)) | ||
Theorem | letric 11336 | Trichotomy law. (Contributed by NM, 18-Aug-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โจ ๐ต โค ๐ด)) | ||
Theorem | ltlen 11337 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ (๐ด โค ๐ต โง ๐ต โ ๐ด))) | ||
Theorem | eqle 11338 | Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.) |
โข ((๐ด โ โ โง ๐ด = ๐ต) โ ๐ด โค ๐ต) | ||
Theorem | eqled 11339 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ ๐ด โค ๐ต) | ||
Theorem | ltadd2 11340 | Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < ๐ต โ (๐ถ + ๐ด) < (๐ถ + ๐ต))) | ||
Theorem | ne0gt0 11341 | A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (๐ด โ 0 โ 0 < ๐ด)) | ||
Theorem | lecasei 11342 | Ordering elimination by cases. (Contributed by NM, 6-Jul-2007.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข ((๐ โง ๐ด โค ๐ต) โ ๐) & โข ((๐ โง ๐ต โค ๐ด) โ ๐) โ โข (๐ โ ๐) | ||
Theorem | lelttric 11343 | Trichotomy law. (Contributed by NM, 4-Apr-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โจ ๐ต < ๐ด)) | ||
Theorem | ltlecasei 11344 | Ordering elimination by cases. (Contributed by NM, 1-Jul-2007.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ โง ๐ด < ๐ต) โ ๐) & โข ((๐ โง ๐ต โค ๐ด) โ ๐) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ ๐) | ||
Theorem | ltnri 11345 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
โข ๐ด โ โ โ โข ยฌ ๐ด < ๐ด | ||
Theorem | eqlei 11346 | Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.) |
โข ๐ด โ โ โ โข (๐ด = ๐ต โ ๐ด โค ๐ต) | ||
Theorem | eqlei2 11347 | Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
โข ๐ด โ โ โ โข (๐ต = ๐ด โ ๐ต โค ๐ด) | ||
Theorem | gtneii 11348 | 'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.) |
โข ๐ด โ โ & โข ๐ด < ๐ต โ โข ๐ต โ ๐ด | ||
Theorem | ltneii 11349 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.) |
โข ๐ด โ โ & โข ๐ด < ๐ต โ โข ๐ด โ ๐ต | ||
Theorem | lttri2i 11350 | Consequence of trichotomy. (Contributed by NM, 19-Jan-1997.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด โ ๐ต โ (๐ด < ๐ต โจ ๐ต < ๐ด)) | ||
Theorem | lttri3i 11351 | Consequence of trichotomy. (Contributed by NM, 14-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด = ๐ต โ (ยฌ ๐ด < ๐ต โง ยฌ ๐ต < ๐ด)) | ||
Theorem | letri3i 11352 | Consequence of trichotomy. (Contributed by NM, 14-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด = ๐ต โ (๐ด โค ๐ต โง ๐ต โค ๐ด)) | ||
Theorem | leloei 11353 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 14-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด โค ๐ต โ (๐ด < ๐ต โจ ๐ด = ๐ต)) | ||
Theorem | ltleni 11354 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด < ๐ต โ (๐ด โค ๐ต โง ๐ต โ ๐ด)) | ||
Theorem | ltnsymi 11355 | 'Less than' is not symmetric. (Contributed by NM, 6-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด < ๐ต โ ยฌ ๐ต < ๐ด) | ||
Theorem | lenlti 11356 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด โค ๐ต โ ยฌ ๐ต < ๐ด) | ||
Theorem | ltnlei 11357 | 'Less than' in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด < ๐ต โ ยฌ ๐ต โค ๐ด) | ||
Theorem | ltlei 11358 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด < ๐ต โ ๐ด โค ๐ต) | ||
Theorem | ltleii 11359 | 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ด < ๐ต โ โข ๐ด โค ๐ต | ||
Theorem | ltnei 11360 | 'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด < ๐ต โ ๐ต โ ๐ด) | ||
Theorem | letrii 11361 | Trichotomy law for 'less than or equal to'. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด โค ๐ต โจ ๐ต โค ๐ด) | ||
Theorem | lttri 11362 | 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((๐ด < ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ) | ||
Theorem | lelttri 11363 | 'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((๐ด โค ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ) | ||
Theorem | ltletri 11364 | 'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((๐ด < ๐ต โง ๐ต โค ๐ถ) โ ๐ด < ๐ถ) | ||
Theorem | letri 11365 | 'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((๐ด โค ๐ต โง ๐ต โค ๐ถ) โ ๐ด โค ๐ถ) | ||
Theorem | le2tri3i 11366 | Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((๐ด โค ๐ต โง ๐ต โค ๐ถ โง ๐ถ โค ๐ด) โ (๐ด = ๐ต โง ๐ต = ๐ถ โง ๐ถ = ๐ด)) | ||
Theorem | ltadd2i 11367 | Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.) (Proof shortened by OpenAI, 25-Mar-2020.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (๐ด < ๐ต โ (๐ถ + ๐ด) < (๐ถ + ๐ต)) | ||
Theorem | mulgt0i 11368 | The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข ((0 < ๐ด โง 0 < ๐ต) โ 0 < (๐ด ยท ๐ต)) | ||
Theorem | mulgt0ii 11369 | The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข 0 < ๐ด & โข 0 < ๐ต โ โข 0 < (๐ด ยท ๐ต) | ||
Theorem | ltnrd 11370 | 'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ยฌ ๐ด < ๐ด) | ||
Theorem | gtned 11371 | 'Less than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ ๐ต โ ๐ด) | ||
Theorem | ltned 11372 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ ๐ด โ ๐ต) | ||
Theorem | ne0gt0d 11373 | A nonzero nonnegative number is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ 0 < ๐ด) | ||
Theorem | lttrid 11374 | Ordering on reals satisfies strict trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด < ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต < ๐ด))) | ||
Theorem | lttri2d 11375 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด โ ๐ต โ (๐ด < ๐ต โจ ๐ต < ๐ด))) | ||
Theorem | lttri3d 11376 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด = ๐ต โ (ยฌ ๐ด < ๐ต โง ยฌ ๐ต < ๐ด))) | ||
Theorem | lttri4d 11377 | Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด < ๐ต โจ ๐ด = ๐ต โจ ๐ต < ๐ด)) | ||
Theorem | letri3d 11378 | Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด = ๐ต โ (๐ด โค ๐ต โง ๐ต โค ๐ด))) | ||
Theorem | leloed 11379 | 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด โค ๐ต โ (๐ด < ๐ต โจ ๐ด = ๐ต))) | ||
Theorem | eqleltd 11380 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด = ๐ต โ (๐ด โค ๐ต โง ยฌ ๐ด < ๐ต))) | ||
Theorem | ltlend 11381 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด < ๐ต โ (๐ด โค ๐ต โง ๐ต โ ๐ด))) | ||
Theorem | lenltd 11382 | 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด โค ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | ltnled 11383 | 'Less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด < ๐ต โ ยฌ ๐ต โค ๐ด)) | ||
Theorem | ltled 11384 | 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ ๐ด โค ๐ต) | ||
Theorem | ltnsymd 11385 | 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ ยฌ ๐ต < ๐ด) | ||
Theorem | nltled 11386 | 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ยฌ ๐ต < ๐ด) โ โข (๐ โ ๐ด โค ๐ต) | ||
Theorem | lensymd 11387 | 'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ ยฌ ๐ต < ๐ด) | ||
Theorem | letrid 11388 | Trichotomy law for 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด โค ๐ต โจ ๐ต โค ๐ด)) | ||
Theorem | leltned 11389 | 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ (๐ด < ๐ต โ ๐ต โ ๐ด)) | ||
Theorem | leneltd 11390 | 'Less than or equal to' and 'not equals' implies 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ต โ ๐ด) โ โข (๐ โ ๐ด < ๐ต) | ||
Theorem | mulgt0d 11391 | The product of two positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 < ๐ด) & โข (๐ โ 0 < ๐ต) โ โข (๐ โ 0 < (๐ด ยท ๐ต)) | ||
Theorem | ltadd2d 11392 | Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (๐ด < ๐ต โ (๐ถ + ๐ด) < (๐ถ + ๐ต))) | ||
Theorem | letrd 11393 | Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ต โค ๐ถ) โ โข (๐ โ ๐ด โค ๐ถ) | ||
Theorem | lelttrd 11394 | Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ต < ๐ถ) โ โข (๐ โ ๐ด < ๐ถ) | ||
Theorem | ltadd2dd 11395 | Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ (๐ถ + ๐ด) < (๐ถ + ๐ต)) | ||
Theorem | ltletrd 11396 | Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ด < ๐ต) & โข (๐ โ ๐ต โค ๐ถ) โ โข (๐ โ ๐ด < ๐ถ) | ||
Theorem | lttrd 11397 | Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ด < ๐ต) & โข (๐ โ ๐ต < ๐ถ) โ โข (๐ โ ๐ด < ๐ถ) | ||
Theorem | lelttrdi 11398 | 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 11399* | The Dedekind cut theorem. This theorem, which may be used to replace ax-pre-sup 11208 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.) |
โข ((๐ด โ โ โง ๐ต โ โ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ < ๐ฆ) โ โ๐ง โ โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต (๐ฅ โค ๐ง โง ๐ง โค ๐ฆ)) | ||
Theorem | dedekindle 11400* | The Dedekind cut theorem, with the hypothesis weakened to only require non-strict less than. (Contributed by Scott Fenton, 2-Jul-2013.) |
โข ((๐ด โ โ โง ๐ต โ โ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ โค ๐ฆ) โ โ๐ง โ โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต (๐ฅ โค ๐ง โง ๐ง โค ๐ฆ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |