Home | Metamath
Proof Explorer Theorem List (p. 112 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | adddii 11101 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)) | ||
Theorem | adddiri 11102 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
โข ๐ด โ โ & โข ๐ต โ โ & โข ๐ถ โ โ โ โข ((๐ด + ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ)) | ||
Theorem | recni 11103 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
โข ๐ด โ โ โ โข ๐ด โ โ | ||
Theorem | readdcli 11104 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด + ๐ต) โ โ | ||
Theorem | remulcli 11105 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ด ยท ๐ต) โ โ | ||
Theorem | mulid1d 11106 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด ยท 1) = ๐ด) | ||
Theorem | mulid2d 11107 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (1 ยท ๐ด) = ๐ด) | ||
Theorem | addcld 11108 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด + ๐ต) โ โ) | ||
Theorem | mulcld 11109 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด ยท ๐ต) โ โ) | ||
Theorem | mulcomd 11110 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) | ||
Theorem | addassd 11111 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ ((๐ด + ๐ต) + ๐ถ) = (๐ด + (๐ต + ๐ถ))) | ||
Theorem | mulassd 11112 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ))) | ||
Theorem | adddid 11113 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))) | ||
Theorem | adddird 11114 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ ((๐ด + ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ))) | ||
Theorem | adddirp1d 11115 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ ((๐ด + 1) ยท ๐ต) = ((๐ด ยท ๐ต) + ๐ต)) | ||
Theorem | joinlmuladdmuld 11116 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ((๐ด ยท ๐ต) + (๐ถ ยท ๐ต)) = ๐ท) โ โข (๐ โ ((๐ด + ๐ถ) ยท ๐ต) = ๐ท) | ||
Theorem | recnd 11117 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | readdcld 11118 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด + ๐ต) โ โ) | ||
Theorem | remulcld 11119 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด ยท ๐ต) โ โ) | ||
Syntax | cpnf 11120 | Plus infinity. |
class +โ | ||
Syntax | cmnf 11121 | Minus infinity. |
class -โ | ||
Syntax | cxr 11122 | The set of extended reals (includes plus and minus infinity). |
class โ* | ||
Syntax | clt 11123 | 'Less than' predicate (extended to include the extended reals). |
class < | ||
Syntax | cle 11124 | Extend wff notation to include the 'less than or equal to' relation. |
class โค | ||
Definition | df-pnf 11125 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that +โ be a set not in โ and different from -โ
(df-mnf 11126). We use ๐ซ โช โ to make it independent of the
construction of โ, and Cantor's Theorem will
show that it is
different from any member of โ and therefore
โ. See pnfnre 11130,
mnfnre 11132, and pnfnemnf 11144.
A simpler possibility is to define +โ as โ and -โ as {โ}, but that approach requires the Axiom of Regularity to show that +โ and -โ are different from each other and from all members of โ. (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
โข +โ = ๐ซ โช โ | ||
Definition | df-mnf 11126 | Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that -โ be a set not in โ and different from +โ (see mnfnre 11132 and pnfnemnf 11144). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
โข -โ = ๐ซ +โ | ||
Definition | df-xr 11127 | Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 13-Oct-2005.) |
โข โ* = (โ โช {+โ, -โ}) | ||
Definition | df-ltxr 11128* | Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. Note that in our postulates for complex numbers, <โ is primitive and not necessarily a relation on โ. (Contributed by NM, 13-Oct-2005.) |
โข < = ({โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ โ โง ๐ฆ โ โ โง ๐ฅ <โ ๐ฆ)} โช (((โ โช {-โ}) ร {+โ}) โช ({-โ} ร โ))) | ||
Definition | df-le 11129 | Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 11175 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.) |
โข โค = ((โ* ร โ*) โ โก < ) | ||
Theorem | pnfnre 11130 | Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
โข +โ โ โ | ||
Theorem | pnfnre2 11131 | Plus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข ยฌ +โ โ โ | ||
Theorem | mnfnre 11132 | Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
โข -โ โ โ | ||
Theorem | ressxr 11133 | The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
โข โ โ โ* | ||
Theorem | rexpssxrxp 11134 | The Cartesian product of standard reals are a subset of the Cartesian product of extended reals. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข (โ ร โ) โ (โ* ร โ*) | ||
Theorem | rexr 11135 | A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ โ ๐ด โ โ*) | ||
Theorem | 0xr 11136 | Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
โข 0 โ โ* | ||
Theorem | renepnf 11137 | No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข (๐ด โ โ โ ๐ด โ +โ) | ||
Theorem | renemnf 11138 | No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข (๐ด โ โ โ ๐ด โ -โ) | ||
Theorem | rexrd 11139 | A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ โ*) | ||
Theorem | renepnfd 11140 | No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ +โ) | ||
Theorem | renemnfd 11141 | No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ -โ) | ||
Theorem | pnfex 11142 | Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018.) (Revised by Steven Nguyen, 7-Dec-2022.) |
โข +โ โ V | ||
Theorem | pnfxr 11143 | Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) |
โข +โ โ โ* | ||
Theorem | pnfnemnf 11144 | Plus and minus infinity are different elements of โ*. (Contributed by NM, 14-Oct-2005.) |
โข +โ โ -โ | ||
Theorem | mnfnepnf 11145 | Minus and plus infinity are different. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข -โ โ +โ | ||
Theorem | mnfxr 11146 | Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข -โ โ โ* | ||
Theorem | rexri 11147 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
โข ๐ด โ โ โ โข ๐ด โ โ* | ||
Theorem | 1xr 11148 | 1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข 1 โ โ* | ||
Theorem | renfdisj 11149 | The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข (โ โฉ {+โ, -โ}) = โ | ||
Theorem | ltrelxr 11150 | "Less than" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
โข < โ (โ* ร โ*) | ||
Theorem | ltrel 11151 | "Less than" is a relation. (Contributed by NM, 14-Oct-2005.) |
โข Rel < | ||
Theorem | lerelxr 11152 | "Less than or equal to" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
โข โค โ (โ* ร โ*) | ||
Theorem | lerel 11153 | "Less than or equal to" is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
โข Rel โค | ||
Theorem | xrlenlt 11154 | "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด โค ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | xrlenltd 11155 | "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) โ โข (๐ โ (๐ด โค ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | xrltnle 11156 | "Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ ยฌ ๐ต โค ๐ด)) | ||
Theorem | xrnltled 11157 | "Not less than" implies "less than or equal to". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ยฌ ๐ต < ๐ด) โ โข (๐ โ ๐ด โค ๐ต) | ||
Theorem | ssxr 11158 | 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 11159 | 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 11160 | 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 11059 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต < ๐ด))) | ||
Theorem | axlttrn 11161 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn 11060 with ordering on the extended reals. New proofs should use lttr 11165 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | axltadd 11162 | 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 11061 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < ๐ต โ (๐ถ + ๐ด) < (๐ถ + ๐ต))) | ||
Theorem | axmulgt0 11163 | 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 11062 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 < ๐ด โง 0 < ๐ต) โ 0 < (๐ด ยท ๐ต))) | ||
Theorem | axsup 11164* | 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 11063 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
โข ((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ < ๐ฅ) โ โ๐ฅ โ โ (โ๐ฆ โ ๐ด ยฌ ๐ฅ < ๐ฆ โง โ๐ฆ โ โ (๐ฆ < ๐ฅ โ โ๐ง โ ๐ด ๐ฆ < ๐ง))) | ||
Theorem | lttr 11165 | Alias for axlttrn 11161, for naming consistency with lttri 11215. New proofs should generally use this instead of ax-pre-lttrn 11060. (Contributed by NM, 10-Mar-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | mulgt0 11166 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
โข (((๐ด โ โ โง 0 < ๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 < (๐ด ยท ๐ต)) | ||
Theorem | lenlt 11167 | 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | ltnle 11168 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ยฌ ๐ต โค ๐ด)) | ||
Theorem | ltso 11169 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
โข < Or โ | ||
Theorem | gtso 11170 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
โข โก < Or โ | ||
Theorem | lttri2 11171 | Consequence of trichotomy. (Contributed by NM, 9-Oct-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โ ๐ต โ (๐ด < ๐ต โจ ๐ต < ๐ด))) | ||
Theorem | lttri3 11172 | Trichotomy law for 'less than'. (Contributed by NM, 5-May-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด = ๐ต โ (ยฌ ๐ด < ๐ต โง ยฌ ๐ต < ๐ด))) | ||
Theorem | lttri4 11173 | Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โจ ๐ด = ๐ต โจ ๐ต < ๐ด)) | ||
Theorem | letri3 11174 | Trichotomy law. (Contributed by NM, 14-May-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด = ๐ต โ (๐ด โค ๐ต โง ๐ต โค ๐ด))) | ||
Theorem | leloe 11175 | 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โ (๐ด < ๐ต โจ ๐ด = ๐ต))) | ||
Theorem | eqlelt 11176 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด = ๐ต โ (๐ด โค ๐ต โง ยฌ ๐ด < ๐ต))) | ||
Theorem | ltle 11177 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ๐ด โค ๐ต)) | ||
Theorem | leltne 11178 | 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด โค ๐ต) โ (๐ด < ๐ต โ ๐ต โ ๐ด)) | ||
Theorem | lelttr 11179 | Transitive law. (Contributed by NM, 23-May-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โค ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | leltletr 11180 | Transitive law, weaker form of lelttr 11179. (Contributed by AV, 14-Oct-2018.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โค ๐ต โง ๐ต < ๐ถ) โ ๐ด โค ๐ถ)) | ||
Theorem | ltletr 11181 | Transitive law. (Contributed by NM, 25-Aug-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ต โง ๐ต โค ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | ltleletr 11182 | Transitive law, weaker form of ltletr 11181. (Contributed by AV, 14-Oct-2018.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ต โง ๐ต โค ๐ถ) โ ๐ด โค ๐ถ)) | ||
Theorem | letr 11183 | Transitive law. (Contributed by NM, 12-Nov-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โค ๐ต โง ๐ต โค ๐ถ) โ ๐ด โค ๐ถ)) | ||
Theorem | ltnr 11184 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
โข (๐ด โ โ โ ยฌ ๐ด < ๐ด) | ||
Theorem | leid 11185 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
โข (๐ด โ โ โ ๐ด โค ๐ด) | ||
Theorem | ltne 11186 | 'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.) |
โข ((๐ด โ โ โง ๐ด < ๐ต) โ ๐ต โ ๐ด) | ||
Theorem | ltnsym 11187 | 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | ltnsym2 11188 | 'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ยฌ (๐ด < ๐ต โง ๐ต < ๐ด)) | ||
Theorem | letric 11189 | Trichotomy law. (Contributed by NM, 18-Aug-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โจ ๐ต โค ๐ด)) | ||
Theorem | ltlen 11190 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ (๐ด โค ๐ต โง ๐ต โ ๐ด))) | ||
Theorem | eqle 11191 | Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.) |
โข ((๐ด โ โ โง ๐ด = ๐ต) โ ๐ด โค ๐ต) | ||
Theorem | eqled 11192 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ ๐ด โค ๐ต) | ||
Theorem | ltadd2 11193 | Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < ๐ต โ (๐ถ + ๐ด) < (๐ถ + ๐ต))) | ||
Theorem | ne0gt0 11194 | A nonzero nonnegative number is positive. (Contributed by NM, 20-Nov-2007.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (๐ด โ 0 โ 0 < ๐ด)) | ||
Theorem | lecasei 11195 | Ordering elimination by cases. (Contributed by NM, 6-Jul-2007.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข ((๐ โง ๐ด โค ๐ต) โ ๐) & โข ((๐ โง ๐ต โค ๐ด) โ ๐) โ โข (๐ โ ๐) | ||
Theorem | lelttric 11196 | Trichotomy law. (Contributed by NM, 4-Apr-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โค ๐ต โจ ๐ต < ๐ด)) | ||
Theorem | ltlecasei 11197 | Ordering elimination by cases. (Contributed by NM, 1-Jul-2007.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
โข ((๐ โง ๐ด < ๐ต) โ ๐) & โข ((๐ โง ๐ต โค ๐ด) โ ๐) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ ๐) | ||
Theorem | ltnri 11198 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
โข ๐ด โ โ โ โข ยฌ ๐ด < ๐ด | ||
Theorem | eqlei 11199 | Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.) |
โข ๐ด โ โ โ โข (๐ด = ๐ต โ ๐ด โค ๐ต) | ||
Theorem | eqlei2 11200 | Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
โข ๐ด โ โ โ โข (๐ต = ๐ด โ ๐ต โค ๐ด) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |