Home | Metamath
Proof Explorer Theorem List (p. 122 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 | rexmul 12101 | The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulf 12102 | The extended real multiplication operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
Theorem | xmulcl 12103 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulpnf1 12104 | Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulpnf2 12105 | Multiplication by plus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulmnf1 12106 | Multiplication by minus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulmnf2 12107 | Multiplication by minus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulpnf1n 12108 | Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulid1 12109 | Extended real version of mulid1 10037. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulid2 12110 | Extended real version of mulid2 10038. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulm1 12111 | Extended real version of mulm1 10471. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulasslem2 12112 | Lemma for xmulass 12117. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulgt0 12113 | Extended real version of mulgt0 10115. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulge0 12114 | Extended real version of mulge0 10546. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulasslem 12115* | Lemma for xmulass 12117. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulasslem3 12116 | Lemma for xmulass 12117. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xmulass 12117 | Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 12079 which has to avoid the "undefined" combinations and . The equivalent "undefined" expression here would be , but since this is defined to equal any zeroes in the expression make the whole thing evaluate to zero (on both sides), thus establishing the identity in this case. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xlemul1a 12118 | Extended real version of lemul1a 10877. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xlemul2a 12119 | Extended real version of lemul2a 10878. (Contributed by Mario Carneiro, 8-Sep-2015.) |
Theorem | xlemul1 12120 | Extended real version of lemul1 10875. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xlemul2 12121 | Extended real version of lemul2 10876. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xltmul1 12122 | Extended real version of ltmul1 10873. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xltmul2 12123 | Extended real version of ltmul2 10874. (Contributed by Mario Carneiro, 8-Sep-2015.) |
Theorem | xadddilem 12124 | Lemma for xadddi 12125. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xadddi 12125 | Distributive property for extended real addition and multiplication. Like xaddass 12079, this has an unusual domain of correctness due to counterexamples like . In this theorem we show that if the multiplier is real then everything works as expected. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xadddir 12126 | Commuted version of xadddi 12125. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xadddi2 12127 | The assumption that the multiplier be real in xadddi 12125 can be relaxed if the addends have the same sign. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xadddi2r 12128 | Commuted version of xadddi2 12127. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | x2times 12129 | Extended real version of 2times 11145. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Theorem | xnegcld 12130 | Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | xaddcld 12131 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | xmulcld 12132 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | xadd4d 12133 | Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 10264. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
Theorem | xnn0add4d 12134 | Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 12133. (Contributed by AV, 12-Dec-2020.) |
NN0* NN0* NN0* NN0* | ||
Theorem | xrsupexmnf 12135* | Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005.) |
Theorem | xrinfmexpnf 12136* | Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006.) |
Theorem | xrsupsslem 12137* | Lemma for xrsupss 12139. (Contributed by NM, 25-Oct-2005.) |
Theorem | xrinfmsslem 12138* | Lemma for xrinfmss 12140. (Contributed by NM, 19-Jan-2006.) |
Theorem | xrsupss 12139* | Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005.) |
Theorem | xrinfmss 12140* | Any subset of extended reals has an infimum. (Contributed by NM, 25-Oct-2005.) |
Theorem | xrinfmss2 12141* | Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | xrub 12142* | By quantifying only over reals, we can specify any extended real upper bound for any set of extended reals. (Contributed by NM, 9-Apr-2006.) |
Theorem | supxr 12143* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) (Revised by Mario Carneiro, 21-Apr-2015.) |
Theorem | supxr2 12144* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) |
Theorem | supxrcl 12145 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 24-Oct-2005.) |
Theorem | supxrun 12146 | The supremum of the union of two sets of extended reals equals the largest of their suprema. (Contributed by NM, 19-Jan-2006.) |
Theorem | supxrmnf 12147 | Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006.) |
Theorem | supxrpnf 12148 | The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005.) |
Theorem | supxrunb1 12149* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
Theorem | supxrunb2 12150* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
Theorem | supxrbnd1 12151* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
Theorem | supxrbnd2 12152* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
Theorem | xrsup0 12153 | The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005.) |
Theorem | supxrub 12154 | A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by NM, 7-Feb-2006.) |
Theorem | supxrlub 12155* | The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by Mario Carneiro, 13-Sep-2015.) |
Theorem | supxrleub 12156* | The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006.) (Revised by Mario Carneiro, 6-Sep-2014.) |
Theorem | supxrre 12157* | The real and extended real suprema match when the real supremum exists. (Contributed by NM, 18-Oct-2005.) (Proof shortened by Mario Carneiro, 7-Sep-2014.) |
Theorem | supxrbnd 12158 | The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006.) |
Theorem | supxrgtmnf 12159 | The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006.) |
Theorem | supxrre1 12160 | The supremum of a nonempty set of reals is real iff it is less than plus infinity. (Contributed by NM, 5-Feb-2006.) |
Theorem | supxrre2 12161 | The supremum of a nonempty set of reals is real iff it is not plus infinity. (Contributed by NM, 5-Feb-2006.) |
Theorem | supxrss 12162 | Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015.) |
Theorem | infxrcl 12163 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 19-Jan-2006.) (Revised by AV, 5-Sep-2020.) |
inf | ||
Theorem | infxrlb 12164 | A member of a set of extended reals is greater than or equal to the set's infimum. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 5-Sep-2020.) |
inf | ||
Theorem | infxrgelb 12165* | The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 5-Sep-2020.) |
inf | ||
Theorem | infxrre 12166* | The real and extended real infima match when the real infimum exists. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 5-Sep-2020.) |
inf inf | ||
Theorem | infxrmnf 12167 | The infinimum of a set of extended reals containing minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
inf | ||
Theorem | xrinf0 12168 | The infimum of the empty set under the extended reals is positive infinity. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by AV, 5-Sep-2020.) |
inf | ||
Theorem | infxrss 12169 | Larger sets of extended reals have smaller infima. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 13-Sep-2020.) |
inf inf | ||
Theorem | reltre 12170* | For all real numbers there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
Theorem | rpltrp 12171* | For all positive real numbers there is a smaller positive real number. (Contributed by AV, 5-Sep-2020.) |
Theorem | reltxrnmnf 12172* | For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
Theorem | infmremnf 12173 | The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020.) |
inf | ||
Theorem | infmrp1 12174 | The infimum of the positive reals is 0. (Contributed by AV, 5-Sep-2020.) |
inf | ||
Syntax | cioo 12175 | Extend class notation with the set of open intervals of extended reals. |
Syntax | cioc 12176 | Extend class notation with the set of open-below, closed-above intervals of extended reals. |
Syntax | cico 12177 | Extend class notation with the set of closed-below, open-above intervals of extended reals. |
Syntax | cicc 12178 | Extend class notation with the set of closed intervals of extended reals. |
Definition | df-ioo 12179* | Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
Definition | df-ioc 12180* | Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
Definition | df-ico 12181* | Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
Definition | df-icc 12182* | Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
Theorem | ixxval 12183* | Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.) |
Theorem | elixx1 12184* | Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
Theorem | ixxf 12185* | The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
Theorem | ixxex 12186* | The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | ixxssxr 12187* | The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.) |
Theorem | elixx3g 12188* | Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show and . (Contributed by Mario Carneiro, 3-Nov-2013.) |
Theorem | ixxssixx 12189* | An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Theorem | ixxdisj 12190* | Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.) |
Theorem | ixxun 12191* | Split an interval into two parts. (Contributed by Mario Carneiro, 16-Jun-2014.) |
Theorem | ixxin 12192* | Intersection of two intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
Theorem | ixxss1 12193* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | ixxss2 12194* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | ixxss12 12195* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | ixxub 12196* | Extract the upper bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) |
Theorem | ixxlb 12197* | Extract the lower bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by AV, 12-Sep-2020.) |
inf | ||
Theorem | iooex 12198 | The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Theorem | iooval 12199* | Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Theorem | ioo0 12200 | An empty open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |