Home | Metamath
Proof Explorer Theorem List (p. 127 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xnegeq 12601 | Equality of two extended numbers with -𝑒 in front of them. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵) | ||
Theorem | xnegex 12602 | A negative extended real exists as a set. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ -𝑒𝐴 ∈ V | ||
Theorem | xnegpnf 12603 | Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) |
⊢ -𝑒+∞ = -∞ | ||
Theorem | xnegmnf 12604 | Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.) |
⊢ -𝑒-∞ = +∞ | ||
Theorem | rexneg 12605 | Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ → -𝑒𝐴 = -𝐴) | ||
Theorem | xneg0 12606 | The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ -𝑒0 = 0 | ||
Theorem | xnegcl 12607 | Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*) | ||
Theorem | xnegneg 12608 | Extended real version of negneg 10936. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴) | ||
Theorem | xneg11 12609 | Extended real version of neg11 10937. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | xltnegi 12610 | Forward direction of xltneg 12611. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴) | ||
Theorem | xltneg 12611 | Extended real version of ltneg 11140. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴)) | ||
Theorem | xleneg 12612 | Extended real version of leneg 11143. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴)) | ||
Theorem | xlt0neg1 12613 | Extended real version of lt0neg1 11146. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴)) | ||
Theorem | xlt0neg2 12614 | Extended real version of lt0neg2 11147. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (0 < 𝐴 ↔ -𝑒𝐴 < 0)) | ||
Theorem | xle0neg1 12615 | Extended real version of le0neg1 11148. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤ -𝑒𝐴)) | ||
Theorem | xle0neg2 12616 | Extended real version of le0neg2 11149. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (𝐴 ∈ ℝ* → (0 ≤ 𝐴 ↔ -𝑒𝐴 ≤ 0)) | ||
Theorem | xaddval 12617 | Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = if(𝐴 = +∞, if(𝐵 = -∞, 0, +∞), if(𝐴 = -∞, if(𝐵 = +∞, 0, -∞), if(𝐵 = +∞, +∞, if(𝐵 = -∞, -∞, (𝐴 + 𝐵)))))) | ||
Theorem | xaddf 12618 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ +𝑒 :(ℝ* × ℝ*)⟶ℝ* | ||
Theorem | xmulval 12619 | 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 12620 | Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞) | ||
Theorem | xaddpnf2 12621 | Addition of positive infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (+∞ +𝑒 𝐴) = +∞) | ||
Theorem | xaddmnf1 12622 | Addition of negative infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞) | ||
Theorem | xaddmnf2 12623 | Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (-∞ +𝑒 𝐴) = -∞) | ||
Theorem | pnfaddmnf 12624 | 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 12625 | 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 12626 | The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) | ||
Theorem | rexsub 12627 | Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 -𝑒𝐵) = (𝐴 − 𝐵)) | ||
Theorem | rexaddd 12628 | The extended real addition operation when both arguments are real. Deduction version of rexadd 12626. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) | ||
Theorem | xnn0xaddcl 12629 | The extended nonnegative integers are closed under extended addition. (Contributed by AV, 10-Dec-2020.) |
⊢ ((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → (𝐴 +𝑒 𝐵) ∈ ℕ0*) | ||
Theorem | xaddnemnf 12630 | Closure of extended real addition in the subset ℝ* / {-∞}. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) → (𝐴 +𝑒 𝐵) ≠ -∞) | ||
Theorem | xaddnepnf 12631 | Closure of extended real addition in the subset ℝ* / {+∞}. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞)) → (𝐴 +𝑒 𝐵) ≠ +∞) | ||
Theorem | xnegid 12632 | Extended real version of negid 10933. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 -𝑒𝐴) = 0) | ||
Theorem | xaddcl 12633 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*) | ||
Theorem | xaddcom 12634 | The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | ||
Theorem | xaddid1 12635 | Extended real version of addid1 10820. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 0) = 𝐴) | ||
Theorem | xaddid2 12636 | Extended real version of addid2 10823. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (0 +𝑒 𝐴) = 𝐴) | ||
Theorem | xaddid1d 12637 | 0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 0) = 𝐴) | ||
Theorem | xnn0lem1lt 12638 | Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0*) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) | ||
Theorem | xnn0lenn0nn0 12639 | 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 12640 | 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 12641 | 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 12642 | Extended real version of negdi 10943. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵)) | ||
Theorem | xaddass 12643 | 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 12644, where +∞ is not present. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
Theorem | xaddass2 12644 | Associativity of extended real addition. See xaddass 12643 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
Theorem | xpncan 12645 | Extended real version of pncan 10892. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 -𝑒𝐵) = 𝐴) | ||
Theorem | xnpcan 12646 | Extended real version of npcan 10895. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) | ||
Theorem | xleadd1a 12647 | Extended real version of leadd1 11108; 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 12648 | Commuted form of xleadd1a 12647. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 +𝑒 𝐴) ≤ (𝐶 +𝑒 𝐵)) | ||
Theorem | xleadd1 12649 | Weakened version of xleadd1a 12647 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))) | ||
Theorem | xltadd1 12650 | Extended real version of ltadd1 11107. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶))) | ||
Theorem | xltadd2 12651 | Extended real version of ltadd2 10744. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 +𝑒 𝐴) < (𝐶 +𝑒 𝐵))) | ||
Theorem | xaddge0 12652 | The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 +𝑒 𝐵)) | ||
Theorem | xle2add 12653 | Extended real version of le2add 11122. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷))) | ||
Theorem | xlt2add 12654 | Extended real version of lt2add 11125. Note that ltleadd 11123, which has weaker assumptions, is not true for the extended reals (since 0 + +∞ < 1 + +∞ fails). (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))) | ||
Theorem | xsubge0 12655 | Extended real version of subge0 11153. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ (𝐴 +𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | xposdif 12656 | Extended real version of posdif 11133. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))) | ||
Theorem | xlesubadd 12657 | Under certain conditions, the conclusion of lesubadd 11112 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵))) | ||
Theorem | xmullem 12658 | Lemma for rexmul 12665. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℝ) | ||
Theorem | xmullem2 12659 | Lemma for xmulneg1 12663. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))))) | ||
Theorem | xmulcom 12660 | Extended real multiplication is commutative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) = (𝐵 ·e 𝐴)) | ||
Theorem | xmul01 12661 | Extended real version of mul01 10819. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 0) = 0) | ||
Theorem | xmul02 12662 | Extended real version of mul02 10818. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (0 ·e 𝐴) = 0) | ||
Theorem | xmulneg1 12663 | Extended real version of mulneg1 11076. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 ·e 𝐵) = -𝑒(𝐴 ·e 𝐵)) | ||
Theorem | xmulneg2 12664 | Extended real version of mulneg2 11077. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e -𝑒𝐵) = -𝑒(𝐴 ·e 𝐵)) | ||
Theorem | rexmul 12665 | The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵)) | ||
Theorem | xmulf 12666 | The extended real multiplication operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ·e :(ℝ* × ℝ*)⟶ℝ* | ||
Theorem | xmulcl 12667 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) ∈ ℝ*) | ||
Theorem | xmulpnf1 12668 | Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e +∞) = +∞) | ||
Theorem | xmulpnf2 12669 | Multiplication by plus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (+∞ ·e 𝐴) = +∞) | ||
Theorem | xmulmnf1 12670 | Multiplication by minus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e -∞) = -∞) | ||
Theorem | xmulmnf2 12671 | Multiplication by minus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (-∞ ·e 𝐴) = -∞) | ||
Theorem | xmulpnf1n 12672 | Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (𝐴 ·e +∞) = -∞) | ||
Theorem | xmulid1 12673 | Extended real version of mulid1 10639. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 1) = 𝐴) | ||
Theorem | xmulid2 12674 | Extended real version of mulid2 10640. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (1 ·e 𝐴) = 𝐴) | ||
Theorem | xmulm1 12675 | Extended real version of mulm1 11081. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (-1 ·e 𝐴) = -𝑒𝐴) | ||
Theorem | xmulasslem2 12676 | Lemma for xmulass 12681. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((0 < 𝐴 ∧ 𝐴 = -∞) → 𝜑) | ||
Theorem | xmulgt0 12677 | Extended real version of mulgt0 10718. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵)) → 0 < (𝐴 ·e 𝐵)) | ||
Theorem | xmulge0 12678 | Extended real version of mulge0 11158. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 ·e 𝐵)) | ||
Theorem | xmulasslem 12679* | Lemma for xmulass 12681. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝑥 = 𝐷 → (𝜓 ↔ 𝑋 = 𝑌)) & ⊢ (𝑥 = -𝑒𝐷 → (𝜓 ↔ 𝐸 = 𝐹)) & ⊢ (𝜑 → 𝑋 ∈ ℝ*) & ⊢ (𝜑 → 𝑌 ∈ ℝ*) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 0 < 𝑥)) → 𝜓) & ⊢ (𝜑 → (𝑥 = 0 → 𝜓)) & ⊢ (𝜑 → 𝐸 = -𝑒𝑋) & ⊢ (𝜑 → 𝐹 = -𝑒𝑌) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | xmulasslem3 12680 | Lemma for xmulass 12681. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 < 𝐶)) → ((𝐴 ·e 𝐵) ·e 𝐶) = (𝐴 ·e (𝐵 ·e 𝐶))) | ||
Theorem | xmulass 12681 | Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 12643 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 12682 | Extended real version of lemul1a 11494. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) | ||
Theorem | xlemul2a 12683 | Extended real version of lemul2a 11495. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 ·e 𝐴) ≤ (𝐶 ·e 𝐵)) | ||
Theorem | xlemul1 12684 | Extended real version of lemul1 11492. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) | ||
Theorem | xlemul2 12685 | Extended real version of lemul2 11493. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐶 ·e 𝐴) ≤ (𝐶 ·e 𝐵))) | ||
Theorem | xltmul1 12686 | Extended real version of ltmul1 11490. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴 ·e 𝐶) < (𝐵 ·e 𝐶))) | ||
Theorem | xltmul2 12687 | Extended real version of ltmul2 11491. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐶 ·e 𝐴) < (𝐶 ·e 𝐵))) | ||
Theorem | xadddilem 12688 | Lemma for xadddi 12689. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 0 < 𝐴) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) | ||
Theorem | xadddi 12689 | Distributive property for extended real addition and multiplication. Like xaddass 12643, 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 12690 | Commuted version of xadddi 12689. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
Theorem | xadddi2 12691 | The assumption that the multiplier be real in xadddi 12689 can be relaxed if the addends have the same sign. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) | ||
Theorem | xadddi2r 12692 | Commuted version of xadddi2 12691. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ*) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
Theorem | x2times 12693 | Extended real version of 2times 11774. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (2 ·e 𝐴) = (𝐴 +𝑒 𝐴)) | ||
Theorem | xnegcld 12694 | Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → -𝑒𝐴 ∈ ℝ*) | ||
Theorem | xaddcld 12695 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈ ℝ*) | ||
Theorem | xmulcld 12696 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ·e 𝐵) ∈ ℝ*) | ||
Theorem | xadd4d 12697 | Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 10868. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞)) & ⊢ (𝜑 → (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) & ⊢ (𝜑 → (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) & ⊢ (𝜑 → (𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞)) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) | ||
Theorem | xnn0add4d 12698 | Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 12697. (Contributed by AV, 12-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0*) & ⊢ (𝜑 → 𝐵 ∈ ℕ0*) & ⊢ (𝜑 → 𝐶 ∈ ℕ0*) & ⊢ (𝜑 → 𝐷 ∈ ℕ0*) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) | ||
Theorem | xrsupexmnf 12699* | Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005.) |
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {-∞}) ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ (𝐴 ∪ {-∞})𝑦 < 𝑧))) | ||
Theorem | xrinfmexpnf 12700* | Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006.) |
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |