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