Home | Metamath
Proof Explorer Theorem List (p. 132 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xleadd2a 13101 | Commuted form of xleadd1a 13100. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ π΄ β€ π΅) β (πΆ +π π΄) β€ (πΆ +π π΅)) | ||
Theorem | xleadd1 13102 | Weakened version of xleadd1a 13100 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β) β (π΄ β€ π΅ β (π΄ +π πΆ) β€ (π΅ +π πΆ))) | ||
Theorem | xltadd1 13103 | Extended real version of ltadd1 11555. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β) β (π΄ < π΅ β (π΄ +π πΆ) < (π΅ +π πΆ))) | ||
Theorem | xltadd2 13104 | Extended real version of ltadd2 11192. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β) β (π΄ < π΅ β (πΆ +π π΄) < (πΆ +π π΅))) | ||
Theorem | xaddge0 13105 | The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (0 β€ π΄ β§ 0 β€ π΅)) β 0 β€ (π΄ +π π΅)) | ||
Theorem | xle2add 13106 | Extended real version of le2add 11570. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (πΆ β β* β§ π· β β*)) β ((π΄ β€ πΆ β§ π΅ β€ π·) β (π΄ +π π΅) β€ (πΆ +π π·))) | ||
Theorem | xlt2add 13107 | Extended real version of lt2add 11573. Note that ltleadd 11571, which has weaker assumptions, is not true for the extended reals (since 0 + +β < 1 + +β fails). (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (πΆ β β* β§ π· β β*)) β ((π΄ < πΆ β§ π΅ < π·) β (π΄ +π π΅) < (πΆ +π π·))) | ||
Theorem | xsubge0 13108 | Extended real version of subge0 11601. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (0 β€ (π΄ +π -ππ΅) β π΅ β€ π΄)) | ||
Theorem | xposdif 13109 | Extended real version of posdif 11581. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ < π΅ β 0 < (π΅ +π -ππ΄))) | ||
Theorem | xlesubadd 13110 | Under certain conditions, the conclusion of lesubadd 11560 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (0 β€ π΄ β§ π΅ β -β β§ 0 β€ πΆ)) β ((π΄ +π -ππ΅) β€ πΆ β π΄ β€ (πΆ +π π΅))) | ||
Theorem | xmullem 13111 | Lemma for rexmul 13118. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((((π΄ β β* β§ π΅ β β*) β§ Β¬ (π΄ = 0 β¨ π΅ = 0)) β§ Β¬ (((0 < π΅ β§ π΄ = +β) β¨ (π΅ < 0 β§ π΄ = -β)) β¨ ((0 < π΄ β§ π΅ = +β) β¨ (π΄ < 0 β§ π΅ = -β)))) β§ Β¬ (((0 < π΅ β§ π΄ = -β) β¨ (π΅ < 0 β§ π΄ = +β)) β¨ ((0 < π΄ β§ π΅ = -β) β¨ (π΄ < 0 β§ π΅ = +β)))) β π΄ β β) | ||
Theorem | xmullem2 13112 | Lemma for xmulneg1 13116. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((((0 < π΅ β§ π΄ = +β) β¨ (π΅ < 0 β§ π΄ = -β)) β¨ ((0 < π΄ β§ π΅ = +β) β¨ (π΄ < 0 β§ π΅ = -β))) β Β¬ (((0 < π΅ β§ π΄ = -β) β¨ (π΅ < 0 β§ π΄ = +β)) β¨ ((0 < π΄ β§ π΅ = -β) β¨ (π΄ < 0 β§ π΅ = +β))))) | ||
Theorem | xmulcom 13113 | Extended real multiplication is commutative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ Β·e π΅) = (π΅ Β·e π΄)) | ||
Theorem | xmul01 13114 | Extended real version of mul01 11267. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (π΄ Β·e 0) = 0) | ||
Theorem | xmul02 13115 | Extended real version of mul02 11266. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (0 Β·e π΄) = 0) | ||
Theorem | xmulneg1 13116 | Extended real version of mulneg1 11524. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (-ππ΄ Β·e π΅) = -π(π΄ Β·e π΅)) | ||
Theorem | xmulneg2 13117 | Extended real version of mulneg2 11525. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ Β·e -ππ΅) = -π(π΄ Β·e π΅)) | ||
Theorem | rexmul 13118 | The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β·e π΅) = (π΄ Β· π΅)) | ||
Theorem | xmulf 13119 | The extended real multiplication operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ Β·e :(β* Γ β*)βΆβ* | ||
Theorem | xmulcl 13120 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ Β·e π΅) β β*) | ||
Theorem | xmulpnf1 13121 | Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (π΄ Β·e +β) = +β) | ||
Theorem | xmulpnf2 13122 | Multiplication by plus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (+β Β·e π΄) = +β) | ||
Theorem | xmulmnf1 13123 | Multiplication by minus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (π΄ Β·e -β) = -β) | ||
Theorem | xmulmnf2 13124 | Multiplication by minus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (-β Β·e π΄) = -β) | ||
Theorem | xmulpnf1n 13125 | Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΄ < 0) β (π΄ Β·e +β) = -β) | ||
Theorem | xmulid1 13126 | Extended real version of mulid1 11086. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (π΄ Β·e 1) = π΄) | ||
Theorem | xmulid2 13127 | Extended real version of mulid2 11087. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (1 Β·e π΄) = π΄) | ||
Theorem | xmulm1 13128 | Extended real version of mulm1 11529. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (-1 Β·e π΄) = -ππ΄) | ||
Theorem | xmulasslem2 13129 | Lemma for xmulass 13134. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((0 < π΄ β§ π΄ = -β) β π) | ||
Theorem | xmulgt0 13130 | Extended real version of mulgt0 11165. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ 0 < π΄) β§ (π΅ β β* β§ 0 < π΅)) β 0 < (π΄ Β·e π΅)) | ||
Theorem | xmulge0 13131 | Extended real version of mulge0 11606. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ 0 β€ π΄) β§ (π΅ β β* β§ 0 β€ π΅)) β 0 β€ (π΄ Β·e π΅)) | ||
Theorem | xmulasslem 13132* | Lemma for xmulass 13134. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π₯ = π· β (π β π = π)) & β’ (π₯ = -ππ· β (π β πΈ = πΉ)) & β’ (π β π β β*) & β’ (π β π β β*) & β’ (π β π· β β*) & β’ ((π β§ (π₯ β β* β§ 0 < π₯)) β π) & β’ (π β (π₯ = 0 β π)) & β’ (π β πΈ = -ππ) & β’ (π β πΉ = -ππ) β β’ (π β π = π) | ||
Theorem | xmulasslem3 13133 | Lemma for xmulass 13134. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ 0 < π΄) β§ (π΅ β β* β§ 0 < π΅) β§ (πΆ β β* β§ 0 < πΆ)) β ((π΄ Β·e π΅) Β·e πΆ) = (π΄ Β·e (π΅ Β·e πΆ))) | ||
Theorem | xmulass 13134 | Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 13096 which has to avoid the "undefined" combinations +β +π -β and -β +π +β. The equivalent "undefined" expression here would be 0 Β·e +β, but since this is defined to equal 0 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.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β ((π΄ Β·e π΅) Β·e πΆ) = (π΄ Β·e (π΅ Β·e πΆ))) | ||
Theorem | xlemul1a 13135 | Extended real version of lemul1a 11942. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ π΅ β β* β§ (πΆ β β* β§ 0 β€ πΆ)) β§ π΄ β€ π΅) β (π΄ Β·e πΆ) β€ (π΅ Β·e πΆ)) | ||
Theorem | xlemul2a 13136 | Extended real version of lemul2a 11943. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ (((π΄ β β* β§ π΅ β β* β§ (πΆ β β* β§ 0 β€ πΆ)) β§ π΄ β€ π΅) β (πΆ Β·e π΄) β€ (πΆ Β·e π΅)) | ||
Theorem | xlemul1 13137 | Extended real version of lemul1 11940. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β+) β (π΄ β€ π΅ β (π΄ Β·e πΆ) β€ (π΅ Β·e πΆ))) | ||
Theorem | xlemul2 13138 | Extended real version of lemul2 11941. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β+) β (π΄ β€ π΅ β (πΆ Β·e π΄) β€ (πΆ Β·e π΅))) | ||
Theorem | xltmul1 13139 | Extended real version of ltmul1 11938. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β+) β (π΄ < π΅ β (π΄ Β·e πΆ) < (π΅ Β·e πΆ))) | ||
Theorem | xltmul2 13140 | Extended real version of ltmul2 11939. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β+) β (π΄ < π΅ β (πΆ Β·e π΄) < (πΆ Β·e π΅))) | ||
Theorem | xadddilem 13141 | Lemma for xadddi 13142. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β β§ π΅ β β* β§ πΆ β β*) β§ 0 < π΄) β (π΄ Β·e (π΅ +π πΆ)) = ((π΄ Β·e π΅) +π (π΄ Β·e πΆ))) | ||
Theorem | xadddi 13142 | Distributive property for extended real addition and multiplication. Like xaddass 13096, this has an unusual domain of correctness due to counterexamples like (+β Β· (2 β 1)) = -β β ((+β Β· 2) β (+β Β· 1)) = (+β β +β) = 0. In this theorem we show that if the multiplier is real then everything works as expected. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β β§ π΅ β β* β§ πΆ β β*) β (π΄ Β·e (π΅ +π πΆ)) = ((π΄ Β·e π΅) +π (π΄ Β·e πΆ))) | ||
Theorem | xadddir 13143 | Commuted version of xadddi 13142. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β) β ((π΄ +π π΅) Β·e πΆ) = ((π΄ Β·e πΆ) +π (π΅ Β·e πΆ))) | ||
Theorem | xadddi2 13144 | The assumption that the multiplier be real in xadddi 13142 can be relaxed if the addends have the same sign. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ (π΅ β β* β§ 0 β€ π΅) β§ (πΆ β β* β§ 0 β€ πΆ)) β (π΄ Β·e (π΅ +π πΆ)) = ((π΄ Β·e π΅) +π (π΄ Β·e πΆ))) | ||
Theorem | xadddi2r 13145 | Commuted version of xadddi2 13144. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ 0 β€ π΄) β§ (π΅ β β* β§ 0 β€ π΅) β§ πΆ β β*) β ((π΄ +π π΅) Β·e πΆ) = ((π΄ Β·e πΆ) +π (π΅ Β·e πΆ))) | ||
Theorem | x2times 13146 | Extended real version of 2times 12222. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (2 Β·e π΄) = (π΄ +π π΄)) | ||
Theorem | xnegcld 13147 | Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.) |
β’ (π β π΄ β β*) β β’ (π β -ππ΄ β β*) | ||
Theorem | xaddcld 13148 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (π΄ +π π΅) β β*) | ||
Theorem | xmulcld 13149 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (π΄ Β·e π΅) β β*) | ||
Theorem | xadd4d 13150 | Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 11316. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
β’ (π β (π΄ β β* β§ π΄ β -β)) & β’ (π β (π΅ β β* β§ π΅ β -β)) & β’ (π β (πΆ β β* β§ πΆ β -β)) & β’ (π β (π· β β* β§ π· β -β)) β β’ (π β ((π΄ +π π΅) +π (πΆ +π π·)) = ((π΄ +π πΆ) +π (π΅ +π π·))) | ||
Theorem | xnn0add4d 13151 | Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 13150. (Contributed by AV, 12-Dec-2020.) |
β’ (π β π΄ β β0*) & β’ (π β π΅ β β0*) & β’ (π β πΆ β β0*) & β’ (π β π· β β0*) β β’ (π β ((π΄ +π π΅) +π (πΆ +π π·)) = ((π΄ +π πΆ) +π (π΅ +π π·))) | ||
Theorem | xrsupexmnf 13152* | Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005.) |
β’ (βπ₯ β β* (βπ¦ β π΄ Β¬ π₯ < π¦ β§ βπ¦ β β* (π¦ < π₯ β βπ§ β π΄ π¦ < π§)) β βπ₯ β β* (βπ¦ β (π΄ βͺ {-β}) Β¬ π₯ < π¦ β§ βπ¦ β β* (π¦ < π₯ β βπ§ β (π΄ βͺ {-β})π¦ < π§))) | ||
Theorem | xrinfmexpnf 13153* | Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006.) |
β’ (βπ₯ β β* (βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β* (π₯ < π¦ β βπ§ β π΄ π§ < π¦)) β βπ₯ β β* (βπ¦ β (π΄ βͺ {+β}) Β¬ π¦ < π₯ β§ βπ¦ β β* (π₯ < π¦ β βπ§ β (π΄ βͺ {+β})π§ < π¦))) | ||
Theorem | xrsupsslem 13154* | Lemma for xrsupss 13156. (Contributed by NM, 25-Oct-2005.) |
β’ ((π΄ β β* β§ (π΄ β β β¨ +β β π΄)) β βπ₯ β β* (βπ¦ β π΄ Β¬ π₯ < π¦ β§ βπ¦ β β* (π¦ < π₯ β βπ§ β π΄ π¦ < π§))) | ||
Theorem | xrinfmsslem 13155* | Lemma for xrinfmss 13157. (Contributed by NM, 19-Jan-2006.) |
β’ ((π΄ β β* β§ (π΄ β β β¨ -β β π΄)) β βπ₯ β β* (βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β* (π₯ < π¦ β βπ§ β π΄ π§ < π¦))) | ||
Theorem | xrsupss 13156* | Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005.) |
β’ (π΄ β β* β βπ₯ β β* (βπ¦ β π΄ Β¬ π₯ < π¦ β§ βπ¦ β β* (π¦ < π₯ β βπ§ β π΄ π¦ < π§))) | ||
Theorem | xrinfmss 13157* | Any subset of extended reals has an infimum. (Contributed by NM, 25-Oct-2005.) |
β’ (π΄ β β* β βπ₯ β β* (βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β* (π₯ < π¦ β βπ§ β π΄ π§ < π¦))) | ||
Theorem | xrinfmss2 13158* | Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ (π΄ β β* β βπ₯ β β* (βπ¦ β π΄ Β¬ π₯β‘ < π¦ β§ βπ¦ β β* (π¦β‘ < π₯ β βπ§ β π΄ π¦β‘ < π§))) | ||
Theorem | xrub 13159* | 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 13160* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) (Revised by Mario Carneiro, 21-Apr-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (βπ₯ β π΄ Β¬ π΅ < π₯ β§ βπ₯ β β (π₯ < π΅ β βπ¦ β π΄ π₯ < π¦))) β sup(π΄, β*, < ) = π΅) | ||
Theorem | supxr2 13161* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (βπ₯ β π΄ π₯ β€ π΅ β§ βπ₯ β β (π₯ < π΅ β βπ¦ β π΄ π₯ < π¦))) β sup(π΄, β*, < ) = π΅) | ||
Theorem | supxrcl 13162 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 24-Oct-2005.) |
β’ (π΄ β β* β sup(π΄, β*, < ) β β*) | ||
Theorem | supxrun 13163 | The supremum of the union of two sets of extended reals equals the largest of their suprema. (Contributed by NM, 19-Jan-2006.) |
β’ ((π΄ β β* β§ π΅ β β* β§ sup(π΄, β*, < ) β€ sup(π΅, β*, < )) β sup((π΄ βͺ π΅), β*, < ) = sup(π΅, β*, < )) | ||
Theorem | supxrmnf 13164 | Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006.) |
β’ (π΄ β β* β sup((π΄ βͺ {-β}), β*, < ) = sup(π΄, β*, < )) | ||
Theorem | supxrpnf 13165 | The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005.) |
β’ ((π΄ β β* β§ +β β π΄) β sup(π΄, β*, < ) = +β) | ||
Theorem | supxrunb1 13166* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π₯ β€ π¦ β sup(π΄, β*, < ) = +β)) | ||
Theorem | supxrunb2 13167* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π₯ < π¦ β sup(π΄, β*, < ) = +β)) | ||
Theorem | supxrbnd1 13168* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ < π₯ β sup(π΄, β*, < ) < +β)) | ||
Theorem | supxrbnd2 13169* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ β€ π₯ β sup(π΄, β*, < ) < +β)) | ||
Theorem | xrsup0 13170 | The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005.) |
β’ sup(β , β*, < ) = -β | ||
Theorem | supxrub 13171 | A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by NM, 7-Feb-2006.) |
β’ ((π΄ β β* β§ π΅ β π΄) β π΅ β€ sup(π΄, β*, < )) | ||
Theorem | supxrlub 13172* | The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΅ < sup(π΄, β*, < ) β βπ₯ β π΄ π΅ < π₯)) | ||
Theorem | supxrleub 13173* | 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.) |
β’ ((π΄ β β* β§ π΅ β β*) β (sup(π΄, β*, < ) β€ π΅ β βπ₯ β π΄ π₯ β€ π΅)) | ||
Theorem | supxrre 13174* | 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.) |
β’ ((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β sup(π΄, β*, < ) = sup(π΄, β, < )) | ||
Theorem | supxrbnd 13175 | The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006.) |
β’ ((π΄ β β β§ π΄ β β β§ sup(π΄, β*, < ) < +β) β sup(π΄, β*, < ) β β) | ||
Theorem | supxrgtmnf 13176 | The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006.) |
β’ ((π΄ β β β§ π΄ β β ) β -β < sup(π΄, β*, < )) | ||
Theorem | supxrre1 13177 | The supremum of a nonempty set of reals is real iff it is less than plus infinity. (Contributed by NM, 5-Feb-2006.) |
β’ ((π΄ β β β§ π΄ β β ) β (sup(π΄, β*, < ) β β β sup(π΄, β*, < ) < +β)) | ||
Theorem | supxrre2 13178 | The supremum of a nonempty set of reals is real iff it is not plus infinity. (Contributed by NM, 5-Feb-2006.) |
β’ ((π΄ β β β§ π΄ β β ) β (sup(π΄, β*, < ) β β β sup(π΄, β*, < ) β +β)) | ||
Theorem | supxrss 13179 | Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015.) |
β’ ((π΄ β π΅ β§ π΅ β β*) β sup(π΄, β*, < ) β€ sup(π΅, β*, < )) | ||
Theorem | infxrcl 13180 | 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 13181 | 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 13182* | 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 13183* | 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 13184 | 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 13185 | 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 13186 | 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 13187* | For all real numbers there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
β’ βπ₯ β β βπ¦ β β π¦ < π₯ | ||
Theorem | rpltrp 13188* | For all positive real numbers there is a smaller positive real number. (Contributed by AV, 5-Sep-2020.) |
β’ βπ₯ β β+ βπ¦ β β+ π¦ < π₯ | ||
Theorem | reltxrnmnf 13189* | For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
β’ βπ₯ β β* (-β < π₯ β βπ¦ β β π¦ < π₯) | ||
Theorem | infmremnf 13190 | The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020.) |
β’ inf(β, β*, < ) = -β | ||
Theorem | infmrp1 13191 | The infimum of the positive reals is 0. (Contributed by AV, 5-Sep-2020.) |
β’ inf(β+, β, < ) = 0 | ||
Syntax | cioo 13192 | Extend class notation with the set of open intervals of extended reals. |
class (,) | ||
Syntax | cioc 13193 | Extend class notation with the set of open-below, closed-above intervals of extended reals. |
class (,] | ||
Syntax | cico 13194 | Extend class notation with the set of closed-below, open-above intervals of extended reals. |
class [,) | ||
Syntax | cicc 13195 | Extend class notation with the set of closed intervals of extended reals. |
class [,] | ||
Definition | df-ioo 13196* | Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ (,) = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) | ||
Definition | df-ioc 13197* | Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ (,] = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ β€ π¦)}) | ||
Definition | df-ico 13198* | Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ [,) = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ < π¦)}) | ||
Definition | df-icc 13199* | Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ [,] = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ β€ π¦)}) | ||
Theorem | ixxval 13200* | Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) β β’ ((π΄ β β* β§ π΅ β β*) β (π΄ππ΅) = {π§ β β* β£ (π΄π π§ β§ π§ππ΅)}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |