![]() |
Metamath
Proof Explorer Theorem List (p. 133 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xlt0neg2 13201 | Extended real version of lt0neg2 11723. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (0 < π΄ β -ππ΄ < 0)) | ||
Theorem | xle0neg1 13202 | Extended real version of le0neg1 11724. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ (π΄ β β* β (π΄ β€ 0 β 0 β€ -ππ΄)) | ||
Theorem | xle0neg2 13203 | Extended real version of le0neg2 11725. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ (π΄ β β* β (0 β€ π΄ β -ππ΄ β€ 0)) | ||
Theorem | xaddval 13204 | Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ +π π΅) = if(π΄ = +β, if(π΅ = -β, 0, +β), if(π΄ = -β, if(π΅ = +β, 0, -β), if(π΅ = +β, +β, if(π΅ = -β, -β, (π΄ + π΅)))))) | ||
Theorem | xaddf 13205 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ +π :(β* Γ β*)βΆβ* | ||
Theorem | xmulval 13206 | Value of the extended real multiplication operation. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ Β·e π΅) = if((π΄ = 0 β¨ π΅ = 0), 0, if((((0 < π΅ β§ π΄ = +β) β¨ (π΅ < 0 β§ π΄ = -β)) β¨ ((0 < π΄ β§ π΅ = +β) β¨ (π΄ < 0 β§ π΅ = -β))), +β, if((((0 < π΅ β§ π΄ = -β) β¨ (π΅ < 0 β§ π΄ = +β)) β¨ ((0 < π΄ β§ π΅ = -β) β¨ (π΄ < 0 β§ π΅ = +β))), -β, (π΄ Β· π΅))))) | ||
Theorem | xaddpnf1 13207 | Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΄ β -β) β (π΄ +π +β) = +β) | ||
Theorem | xaddpnf2 13208 | Addition of positive infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΄ β -β) β (+β +π π΄) = +β) | ||
Theorem | xaddmnf1 13209 | Addition of negative infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΄ β +β) β (π΄ +π -β) = -β) | ||
Theorem | xaddmnf2 13210 | Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΄ β +β) β (-β +π π΄) = -β) | ||
Theorem | pnfaddmnf 13211 | Addition of positive and negative infinity. This is often taken to be a "null" value or out of the domain, but we define it (somewhat arbitrarily) to be zero so that the resulting function is total, which simplifies proofs. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (+β +π -β) = 0 | ||
Theorem | mnfaddpnf 13212 | Addition of negative and positive infinity. This is often taken to be a "null" value or out of the domain, but we define it (somewhat arbitrarily) to be zero so that the resulting function is total, which simplifies proofs. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (-β +π +β) = 0 | ||
Theorem | rexadd 13213 | The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +π π΅) = (π΄ + π΅)) | ||
Theorem | rexsub 13214 | Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ +π -ππ΅) = (π΄ β π΅)) | ||
Theorem | rexaddd 13215 | The extended real addition operation when both arguments are real. Deduction version of rexadd 13213. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄ +π π΅) = (π΄ + π΅)) | ||
Theorem | xnn0xaddcl 13216 | The extended nonnegative integers are closed under extended addition. (Contributed by AV, 10-Dec-2020.) |
β’ ((π΄ β β0* β§ π΅ β β0*) β (π΄ +π π΅) β β0*) | ||
Theorem | xaddnemnf 13217 | Closure of extended real addition in the subset β* / {-β}. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ π΄ β -β) β§ (π΅ β β* β§ π΅ β -β)) β (π΄ +π π΅) β -β) | ||
Theorem | xaddnepnf 13218 | Closure of extended real addition in the subset β* / {+β}. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ π΄ β +β) β§ (π΅ β β* β§ π΅ β +β)) β (π΄ +π π΅) β +β) | ||
Theorem | xnegid 13219 | Extended real version of negid 11509. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (π΄ +π -ππ΄) = 0) | ||
Theorem | xaddcl 13220 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ +π π΅) β β*) | ||
Theorem | xaddcom 13221 | The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ +π π΅) = (π΅ +π π΄)) | ||
Theorem | xaddrid 13222 | Extended real version of addrid 11396. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (π΄ +π 0) = π΄) | ||
Theorem | xaddlid 13223 | Extended real version of addlid 11399. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (0 +π π΄) = π΄) | ||
Theorem | xaddridd 13224 | 0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) β β’ (π β (π΄ +π 0) = π΄) | ||
Theorem | xnn0lem1lt 13225 | Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ ((π β β0 β§ π β β0*) β (π β€ π β (π β 1) < π)) | ||
Theorem | xnn0lenn0nn0 13226 | An extended nonnegative integer which is less than or equal to a nonnegative integer is a nonnegative integer. (Contributed by AV, 24-Nov-2021.) |
β’ ((π β β0* β§ π β β0 β§ π β€ π) β π β β0) | ||
Theorem | xnn0le2is012 13227 | An extended nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 24-Nov-2021.) |
β’ ((π β β0* β§ π β€ 2) β (π = 0 β¨ π = 1 β¨ π = 2)) | ||
Theorem | xnn0xadd0 13228 | The sum of two extended nonnegative integers is 0 iff each of the two extended nonnegative integers is 0. (Contributed by AV, 14-Dec-2020.) |
β’ ((π΄ β β0* β§ π΅ β β0*) β ((π΄ +π π΅) = 0 β (π΄ = 0 β§ π΅ = 0))) | ||
Theorem | xnegdi 13229 | Extended real version of negdi 11519. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β -π(π΄ +π π΅) = (-ππ΄ +π -ππ΅)) | ||
Theorem | xaddass 13230 | Associativity of extended real addition. The correct condition here is "it is not the case that both +β and -β appear as one of π΄, π΅, πΆ, i.e. Β¬ {+β, -β} β {π΄, π΅, πΆ}", but this condition is difficult to work with, so we break the theorem into two parts: this one, where -β is not present in π΄, π΅, πΆ, and xaddass2 13231, where +β is not present. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ π΄ β -β) β§ (π΅ β β* β§ π΅ β -β) β§ (πΆ β β* β§ πΆ β -β)) β ((π΄ +π π΅) +π πΆ) = (π΄ +π (π΅ +π πΆ))) | ||
Theorem | xaddass2 13231 | Associativity of extended real addition. See xaddass 13230 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ π΄ β +β) β§ (π΅ β β* β§ π΅ β +β) β§ (πΆ β β* β§ πΆ β +β)) β ((π΄ +π π΅) +π πΆ) = (π΄ +π (π΅ +π πΆ))) | ||
Theorem | xpncan 13232 | Extended real version of pncan 11468. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β) β ((π΄ +π π΅) +π -ππ΅) = π΄) | ||
Theorem | xnpcan 13233 | Extended real version of npcan 11471. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β) β ((π΄ +π -ππ΅) +π π΅) = π΄) | ||
Theorem | xleadd1a 13234 | Extended real version of leadd1 11684; 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 13235 | Commuted form of xleadd1a 13234. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ π΄ β€ π΅) β (πΆ +π π΄) β€ (πΆ +π π΅)) | ||
Theorem | xleadd1 13236 | Weakened version of xleadd1a 13234 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β) β (π΄ β€ π΅ β (π΄ +π πΆ) β€ (π΅ +π πΆ))) | ||
Theorem | xltadd1 13237 | Extended real version of ltadd1 11683. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β) β (π΄ < π΅ β (π΄ +π πΆ) < (π΅ +π πΆ))) | ||
Theorem | xltadd2 13238 | Extended real version of ltadd2 11320. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β) β (π΄ < π΅ β (πΆ +π π΄) < (πΆ +π π΅))) | ||
Theorem | xaddge0 13239 | The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (0 β€ π΄ β§ 0 β€ π΅)) β 0 β€ (π΄ +π π΅)) | ||
Theorem | xle2add 13240 | Extended real version of le2add 11698. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (πΆ β β* β§ π· β β*)) β ((π΄ β€ πΆ β§ π΅ β€ π·) β (π΄ +π π΅) β€ (πΆ +π π·))) | ||
Theorem | xlt2add 13241 | Extended real version of lt2add 11701. Note that ltleadd 11699, which has weaker assumptions, is not true for the extended reals (since 0 + +β < 1 + +β fails). (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (πΆ β β* β§ π· β β*)) β ((π΄ < πΆ β§ π΅ < π·) β (π΄ +π π΅) < (πΆ +π π·))) | ||
Theorem | xsubge0 13242 | Extended real version of subge0 11729. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (0 β€ (π΄ +π -ππ΅) β π΅ β€ π΄)) | ||
Theorem | xposdif 13243 | Extended real version of posdif 11709. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ < π΅ β 0 < (π΅ +π -ππ΄))) | ||
Theorem | xlesubadd 13244 | Under certain conditions, the conclusion of lesubadd 11688 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (0 β€ π΄ β§ π΅ β -β β§ 0 β€ πΆ)) β ((π΄ +π -ππ΅) β€ πΆ β π΄ β€ (πΆ +π π΅))) | ||
Theorem | xmullem 13245 | Lemma for rexmul 13252. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((((π΄ β β* β§ π΅ β β*) β§ Β¬ (π΄ = 0 β¨ π΅ = 0)) β§ Β¬ (((0 < π΅ β§ π΄ = +β) β¨ (π΅ < 0 β§ π΄ = -β)) β¨ ((0 < π΄ β§ π΅ = +β) β¨ (π΄ < 0 β§ π΅ = -β)))) β§ Β¬ (((0 < π΅ β§ π΄ = -β) β¨ (π΅ < 0 β§ π΄ = +β)) β¨ ((0 < π΄ β§ π΅ = -β) β¨ (π΄ < 0 β§ π΅ = +β)))) β π΄ β β) | ||
Theorem | xmullem2 13246 | Lemma for xmulneg1 13250. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((((0 < π΅ β§ π΄ = +β) β¨ (π΅ < 0 β§ π΄ = -β)) β¨ ((0 < π΄ β§ π΅ = +β) β¨ (π΄ < 0 β§ π΅ = -β))) β Β¬ (((0 < π΅ β§ π΄ = -β) β¨ (π΅ < 0 β§ π΄ = +β)) β¨ ((0 < π΄ β§ π΅ = -β) β¨ (π΄ < 0 β§ π΅ = +β))))) | ||
Theorem | xmulcom 13247 | Extended real multiplication is commutative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ Β·e π΅) = (π΅ Β·e π΄)) | ||
Theorem | xmul01 13248 | Extended real version of mul01 11395. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (π΄ Β·e 0) = 0) | ||
Theorem | xmul02 13249 | Extended real version of mul02 11394. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (0 Β·e π΄) = 0) | ||
Theorem | xmulneg1 13250 | Extended real version of mulneg1 11652. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (-ππ΄ Β·e π΅) = -π(π΄ Β·e π΅)) | ||
Theorem | xmulneg2 13251 | Extended real version of mulneg2 11653. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ Β·e -ππ΅) = -π(π΄ Β·e π΅)) | ||
Theorem | rexmul 13252 | The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β·e π΅) = (π΄ Β· π΅)) | ||
Theorem | xmulf 13253 | The extended real multiplication operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ Β·e :(β* Γ β*)βΆβ* | ||
Theorem | xmulcl 13254 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ Β·e π΅) β β*) | ||
Theorem | xmulpnf1 13255 | Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (π΄ Β·e +β) = +β) | ||
Theorem | xmulpnf2 13256 | Multiplication by plus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (+β Β·e π΄) = +β) | ||
Theorem | xmulmnf1 13257 | Multiplication by minus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (π΄ Β·e -β) = -β) | ||
Theorem | xmulmnf2 13258 | Multiplication by minus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (-β Β·e π΄) = -β) | ||
Theorem | xmulpnf1n 13259 | Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΄ < 0) β (π΄ Β·e +β) = -β) | ||
Theorem | xmulrid 13260 | Extended real version of mulrid 11214. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (π΄ Β·e 1) = π΄) | ||
Theorem | xmullid 13261 | Extended real version of mullid 11215. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (1 Β·e π΄) = π΄) | ||
Theorem | xmulm1 13262 | Extended real version of mulm1 11657. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (-1 Β·e π΄) = -ππ΄) | ||
Theorem | xmulasslem2 13263 | Lemma for xmulass 13268. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((0 < π΄ β§ π΄ = -β) β π) | ||
Theorem | xmulgt0 13264 | Extended real version of mulgt0 11293. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ 0 < π΄) β§ (π΅ β β* β§ 0 < π΅)) β 0 < (π΄ Β·e π΅)) | ||
Theorem | xmulge0 13265 | Extended real version of mulge0 11734. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ 0 β€ π΄) β§ (π΅ β β* β§ 0 β€ π΅)) β 0 β€ (π΄ Β·e π΅)) | ||
Theorem | xmulasslem 13266* | Lemma for xmulass 13268. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π₯ = π· β (π β π = π)) & β’ (π₯ = -ππ· β (π β πΈ = πΉ)) & β’ (π β π β β*) & β’ (π β π β β*) & β’ (π β π· β β*) & β’ ((π β§ (π₯ β β* β§ 0 < π₯)) β π) & β’ (π β (π₯ = 0 β π)) & β’ (π β πΈ = -ππ) & β’ (π β πΉ = -ππ) β β’ (π β π = π) | ||
Theorem | xmulasslem3 13267 | Lemma for xmulass 13268. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ 0 < π΄) β§ (π΅ β β* β§ 0 < π΅) β§ (πΆ β β* β§ 0 < πΆ)) β ((π΄ Β·e π΅) Β·e πΆ) = (π΄ Β·e (π΅ Β·e πΆ))) | ||
Theorem | xmulass 13268 | Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 13230 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 13269 | Extended real version of lemul1a 12070. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ π΅ β β* β§ (πΆ β β* β§ 0 β€ πΆ)) β§ π΄ β€ π΅) β (π΄ Β·e πΆ) β€ (π΅ Β·e πΆ)) | ||
Theorem | xlemul2a 13270 | Extended real version of lemul2a 12071. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ (((π΄ β β* β§ π΅ β β* β§ (πΆ β β* β§ 0 β€ πΆ)) β§ π΄ β€ π΅) β (πΆ Β·e π΄) β€ (πΆ Β·e π΅)) | ||
Theorem | xlemul1 13271 | Extended real version of lemul1 12068. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β+) β (π΄ β€ π΅ β (π΄ Β·e πΆ) β€ (π΅ Β·e πΆ))) | ||
Theorem | xlemul2 13272 | Extended real version of lemul2 12069. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β+) β (π΄ β€ π΅ β (πΆ Β·e π΄) β€ (πΆ Β·e π΅))) | ||
Theorem | xltmul1 13273 | Extended real version of ltmul1 12066. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β+) β (π΄ < π΅ β (π΄ Β·e πΆ) < (π΅ Β·e πΆ))) | ||
Theorem | xltmul2 13274 | Extended real version of ltmul2 12067. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β+) β (π΄ < π΅ β (πΆ Β·e π΄) < (πΆ Β·e π΅))) | ||
Theorem | xadddilem 13275 | Lemma for xadddi 13276. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β β§ π΅ β β* β§ πΆ β β*) β§ 0 < π΄) β (π΄ Β·e (π΅ +π πΆ)) = ((π΄ Β·e π΅) +π (π΄ Β·e πΆ))) | ||
Theorem | xadddi 13276 | Distributive property for extended real addition and multiplication. Like xaddass 13230, 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 13277 | Commuted version of xadddi 13276. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β) β ((π΄ +π π΅) Β·e πΆ) = ((π΄ Β·e πΆ) +π (π΅ Β·e πΆ))) | ||
Theorem | xadddi2 13278 | The assumption that the multiplier be real in xadddi 13276 can be relaxed if the addends have the same sign. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ((π΄ β β* β§ (π΅ β β* β§ 0 β€ π΅) β§ (πΆ β β* β§ 0 β€ πΆ)) β (π΄ Β·e (π΅ +π πΆ)) = ((π΄ Β·e π΅) +π (π΄ Β·e πΆ))) | ||
Theorem | xadddi2r 13279 | Commuted version of xadddi2 13278. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (((π΄ β β* β§ 0 β€ π΄) β§ (π΅ β β* β§ 0 β€ π΅) β§ πΆ β β*) β ((π΄ +π π΅) Β·e πΆ) = ((π΄ Β·e πΆ) +π (π΅ Β·e πΆ))) | ||
Theorem | x2times 13280 | Extended real version of 2times 12350. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ (π΄ β β* β (2 Β·e π΄) = (π΄ +π π΄)) | ||
Theorem | xnegcld 13281 | Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.) |
β’ (π β π΄ β β*) β β’ (π β -ππ΄ β β*) | ||
Theorem | xaddcld 13282 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (π΄ +π π΅) β β*) | ||
Theorem | xmulcld 13283 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (π΄ Β·e π΅) β β*) | ||
Theorem | xadd4d 13284 | Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 11444. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
β’ (π β (π΄ β β* β§ π΄ β -β)) & β’ (π β (π΅ β β* β§ π΅ β -β)) & β’ (π β (πΆ β β* β§ πΆ β -β)) & β’ (π β (π· β β* β§ π· β -β)) β β’ (π β ((π΄ +π π΅) +π (πΆ +π π·)) = ((π΄ +π πΆ) +π (π΅ +π π·))) | ||
Theorem | xnn0add4d 13285 | Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 13284. (Contributed by AV, 12-Dec-2020.) |
β’ (π β π΄ β β0*) & β’ (π β π΅ β β0*) & β’ (π β πΆ β β0*) & β’ (π β π· β β0*) β β’ (π β ((π΄ +π π΅) +π (πΆ +π π·)) = ((π΄ +π πΆ) +π (π΅ +π π·))) | ||
Theorem | xrsupexmnf 13286* | Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005.) |
β’ (βπ₯ β β* (βπ¦ β π΄ Β¬ π₯ < π¦ β§ βπ¦ β β* (π¦ < π₯ β βπ§ β π΄ π¦ < π§)) β βπ₯ β β* (βπ¦ β (π΄ βͺ {-β}) Β¬ π₯ < π¦ β§ βπ¦ β β* (π¦ < π₯ β βπ§ β (π΄ βͺ {-β})π¦ < π§))) | ||
Theorem | xrinfmexpnf 13287* | Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006.) |
β’ (βπ₯ β β* (βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β* (π₯ < π¦ β βπ§ β π΄ π§ < π¦)) β βπ₯ β β* (βπ¦ β (π΄ βͺ {+β}) Β¬ π¦ < π₯ β§ βπ¦ β β* (π₯ < π¦ β βπ§ β (π΄ βͺ {+β})π§ < π¦))) | ||
Theorem | xrsupsslem 13288* | Lemma for xrsupss 13290. (Contributed by NM, 25-Oct-2005.) |
β’ ((π΄ β β* β§ (π΄ β β β¨ +β β π΄)) β βπ₯ β β* (βπ¦ β π΄ Β¬ π₯ < π¦ β§ βπ¦ β β* (π¦ < π₯ β βπ§ β π΄ π¦ < π§))) | ||
Theorem | xrinfmsslem 13289* | Lemma for xrinfmss 13291. (Contributed by NM, 19-Jan-2006.) |
β’ ((π΄ β β* β§ (π΄ β β β¨ -β β π΄)) β βπ₯ β β* (βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β* (π₯ < π¦ β βπ§ β π΄ π§ < π¦))) | ||
Theorem | xrsupss 13290* | Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005.) |
β’ (π΄ β β* β βπ₯ β β* (βπ¦ β π΄ Β¬ π₯ < π¦ β§ βπ¦ β β* (π¦ < π₯ β βπ§ β π΄ π¦ < π§))) | ||
Theorem | xrinfmss 13291* | Any subset of extended reals has an infimum. (Contributed by NM, 25-Oct-2005.) |
β’ (π΄ β β* β βπ₯ β β* (βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β* (π₯ < π¦ β βπ§ β π΄ π§ < π¦))) | ||
Theorem | xrinfmss2 13292* | Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ (π΄ β β* β βπ₯ β β* (βπ¦ β π΄ Β¬ π₯β‘ < π¦ β§ βπ¦ β β* (π¦β‘ < π₯ β βπ§ β π΄ π¦β‘ < π§))) | ||
Theorem | xrub 13293* | 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 13294* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) (Revised by Mario Carneiro, 21-Apr-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (βπ₯ β π΄ Β¬ π΅ < π₯ β§ βπ₯ β β (π₯ < π΅ β βπ¦ β π΄ π₯ < π¦))) β sup(π΄, β*, < ) = π΅) | ||
Theorem | supxr2 13295* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (βπ₯ β π΄ π₯ β€ π΅ β§ βπ₯ β β (π₯ < π΅ β βπ¦ β π΄ π₯ < π¦))) β sup(π΄, β*, < ) = π΅) | ||
Theorem | supxrcl 13296 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 24-Oct-2005.) |
β’ (π΄ β β* β sup(π΄, β*, < ) β β*) | ||
Theorem | supxrun 13297 | 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 13298 | Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006.) |
β’ (π΄ β β* β sup((π΄ βͺ {-β}), β*, < ) = sup(π΄, β*, < )) | ||
Theorem | supxrpnf 13299 | The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005.) |
β’ ((π΄ β β* β§ +β β π΄) β sup(π΄, β*, < ) = +β) | ||
Theorem | supxrunb1 13300* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π₯ β€ π¦ β sup(π΄, β*, < ) = +β)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |