HomeTheorem List (p. 130 of 466)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 130 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | xrletr 12901 | Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) | ||
| Theorem | xrlttrd 12902 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | xrlelttrd 12903 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | xrltletrd 12904 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | xrletrd 12905 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) | ||
| Theorem | xrltne 12906 | 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) | ||
| Theorem | nltpnft 12907 | An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) | ||
| Theorem | xgepnf 12908 | An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ (𝐴 ∈ ℝ* → (+∞ ≤ 𝐴 ↔ 𝐴 = +∞)) | ||
| Theorem | ngtmnft 12909 | An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴)) | ||
| Theorem | xlemnf 12910 | An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ -∞ ↔ 𝐴 = -∞)) | ||
| Theorem | xrrebnd 12911 | An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴 ∧ 𝐴 < +∞))) | ||
| Theorem | xrre 12912 | A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) | ||
| Theorem | xrre2 12913 | An extended real between two others is real. (Contributed by NM, 6-Feb-2007.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ) | ||
| Theorem | xrre3 12914 | A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < +∞)) → 𝐴 ∈ ℝ) | ||
| Theorem | ge0gtmnf 12915 | A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → -∞ < 𝐴) | ||
| Theorem | ge0nemnf 12916 | A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≠ -∞) | ||
| Theorem | xrrege0 12917 | A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) | ||
| Theorem | xrmax1 12918 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | xrmax2 12919 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | xrmin1 12920 | The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴) | ||
| Theorem | xrmin2 12921 | The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵) | ||
| Theorem | xrmaxeq 12922 | The maximum of two extended reals is equal to the first if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐴) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = 𝐴) | ||
| Theorem | xrmineq 12923 | The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐴) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) = 𝐵) | ||
| Theorem | xrmaxlt 12924 | Two ways of saying the maximum of two extended reals is less than a third. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) | ||
| Theorem | xrltmin 12925 | Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶))) | ||
| Theorem | xrmaxle 12926 | Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) ≤ 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶))) | ||
| Theorem | xrlemin 12927 | Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ≤ if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶))) | ||
| Theorem | max1 12928 | A number is less than or equal to the maximum of it and another. See also max1ALT 12929. (Contributed by NM, 3-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | max1ALT 12929 | A number is less than or equal to the maximum of it and another. This version of max1 12928 omits the 𝐵 ∈ ℝ antecedent. Although it doesn't exploit undefined behavior, it is still considered poor style, and the use of max1 12928 is preferred. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 3-Apr-2005.) |
| ⊢ (𝐴 ∈ ℝ → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | max2 12930 | A number is less than or equal to the maximum of it and another. (Contributed by NM, 3-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | 2resupmax 12931 | The supremum of two real numbers is the maximum of these two numbers. (Contributed by AV, 8-Jun-2021.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | min1 12932 | The minimum of two numbers is less than or equal to the first. (Contributed by NM, 3-Aug-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴) | ||
| Theorem | min2 12933 | The minimum of two numbers is less than or equal to the second. (Contributed by NM, 3-Aug-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵) | ||
| Theorem | maxle 12934 | Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by NM, 29-Sep-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) ≤ 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶))) | ||
| Theorem | lemin 12935 | Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by NM, 3-Aug-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶))) | ||
| Theorem | maxlt 12936 | Two ways of saying the maximum of two numbers is less than a third. (Contributed by NM, 3-Aug-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) | ||
| Theorem | ltmin 12937 | Two ways of saying a number is less than the minimum of two others. (Contributed by NM, 1-Sep-2006.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶))) | ||
| Theorem | lemaxle 12938 | A real number which is less than or equal to a second real number is less than or equal to the maximum/supremum of the second real number and a third real number. (Contributed by AV, 8-Jun-2021.) |
| ⊢ (((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ if(𝐶 ≤ 𝐵, 𝐵, 𝐶)) | ||
| Theorem | max0sub 12939 | Decompose a real number into positive and negative parts. (Contributed by Mario Carneiro, 6-Aug-2014.) |
| ⊢ (𝐴 ∈ ℝ → (if(0 ≤ 𝐴, 𝐴, 0) − if(0 ≤ -𝐴, -𝐴, 0)) = 𝐴) | ||
| Theorem | ifle 12940 | An if statement transforms an implication into an inequality of terms. (Contributed by Mario Carneiro, 31-Aug-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≤ 𝐴) ∧ (𝜑 → 𝜓)) → if(𝜑, 𝐴, 𝐵) ≤ if(𝜓, 𝐴, 𝐵)) | ||
| Theorem | z2ge 12941* | There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘)) | ||
| Theorem | qbtwnre 12942* | The rational numbers are dense in ℝ: any two real numbers have a rational between them. Exercise 6 of [Apostol] p. 28. (Contributed by NM, 18-Nov-2004.) (Proof shortened by Mario Carneiro, 13-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) | ||
| Theorem | qbtwnxr 12943* | The rational numbers are dense in ℝ*: any two extended real numbers have a rational between them. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) | ||
| Theorem | qsqueeze 12944* | If a nonnegative real is less than any positive rational, it is zero. (Contributed by NM, 6-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℚ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0) | ||
| Theorem | qextltlem 12945* | Lemma for qextlt 12946 and qextle . (Contributed by Mario Carneiro, 3-Oct-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))) | ||
| Theorem | qextlt 12946* | An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵))) | ||
| Theorem | qextle 12947* | An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵))) | ||
| Theorem | xralrple 12948* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Mario Carneiro, 12-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + 𝑥))) | ||
| Theorem | alrple 12949* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Mario Carneiro, 12-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + 𝑥))) | ||
| Theorem | xnegeq 12950 | 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 12951 | A negative extended real exists as a set. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ -𝑒𝐴 ∈ V | ||
| Theorem | xnegpnf 12952 | Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) |
| ⊢ -𝑒+∞ = -∞ | ||
| Theorem | xnegmnf 12953 | Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.) |
| ⊢ -𝑒-∞ = +∞ | ||
| Theorem | rexneg 12954 | 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 12955 | The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ -𝑒0 = 0 | ||
| Theorem | xnegcl 12956 | Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*) | ||
| Theorem | xnegneg 12957 | Extended real version of negneg 11280. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴) | ||
| Theorem | xneg11 12958 | Extended real version of neg11 11281. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | xltnegi 12959 | Forward direction of xltneg 12960. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴) | ||
| Theorem | xltneg 12960 | Extended real version of ltneg 11484. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴)) | ||
| Theorem | xleneg 12961 | Extended real version of leneg 11487. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴)) | ||
| Theorem | xlt0neg1 12962 | Extended real version of lt0neg1 11490. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴)) | ||
| Theorem | xlt0neg2 12963 | Extended real version of lt0neg2 11491. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (0 < 𝐴 ↔ -𝑒𝐴 < 0)) | ||
| Theorem | xle0neg1 12964 | Extended real version of le0neg1 11492. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤ -𝑒𝐴)) | ||
| Theorem | xle0neg2 12965 | Extended real version of le0neg2 11493. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (0 ≤ 𝐴 ↔ -𝑒𝐴 ≤ 0)) | ||
| Theorem | xaddval 12966 | Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = if(𝐴 = +∞, if(𝐵 = -∞, 0, +∞), if(𝐴 = -∞, if(𝐵 = +∞, 0, -∞), if(𝐵 = +∞, +∞, if(𝐵 = -∞, -∞, (𝐴 + 𝐵)))))) | ||
| Theorem | xaddf 12967 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ +𝑒 :(ℝ* × ℝ*)⟶ℝ* | ||
| Theorem | xmulval 12968 | 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 12969 | Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞) | ||
| Theorem | xaddpnf2 12970 | Addition of positive infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (+∞ +𝑒 𝐴) = +∞) | ||
| Theorem | xaddmnf1 12971 | Addition of negative infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞) | ||
| Theorem | xaddmnf2 12972 | Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (-∞ +𝑒 𝐴) = -∞) | ||
| Theorem | pnfaddmnf 12973 | 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 12974 | 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 12975 | The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) | ||
| Theorem | rexsub 12976 | Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 -𝑒𝐵) = (𝐴 − 𝐵)) | ||
| Theorem | rexaddd 12977 | The extended real addition operation when both arguments are real. Deduction version of rexadd 12975. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) | ||
| Theorem | xnn0xaddcl 12978 | The extended nonnegative integers are closed under extended addition. (Contributed by AV, 10-Dec-2020.) |
| ⊢ ((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → (𝐴 +𝑒 𝐵) ∈ ℕ0*) | ||
| Theorem | xaddnemnf 12979 | Closure of extended real addition in the subset ℝ* / {-∞}. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) → (𝐴 +𝑒 𝐵) ≠ -∞) | ||
| Theorem | xaddnepnf 12980 | Closure of extended real addition in the subset ℝ* / {+∞}. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞)) → (𝐴 +𝑒 𝐵) ≠ +∞) | ||
| Theorem | xnegid 12981 | Extended real version of negid 11277. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 -𝑒𝐴) = 0) | ||
| Theorem | xaddcl 12982 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*) | ||
| Theorem | xaddcom 12983 | The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | ||
| Theorem | xaddid1 12984 | Extended real version of addid1 11164. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 0) = 𝐴) | ||
| Theorem | xaddid2 12985 | Extended real version of addid2 11167. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (0 +𝑒 𝐴) = 𝐴) | ||
| Theorem | xaddid1d 12986 | 0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 0) = 𝐴) | ||
| Theorem | xnn0lem1lt 12987 | Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0*) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) | ||
| Theorem | xnn0lenn0nn0 12988 | 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 12989 | 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 12990 | 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 12991 | Extended real version of negdi 11287. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵)) | ||
| Theorem | xaddass 12992 | 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 12993, where +∞ is not present. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
| Theorem | xaddass2 12993 | Associativity of extended real addition. See xaddass 12992 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
| Theorem | xpncan 12994 | Extended real version of pncan 11236. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 -𝑒𝐵) = 𝐴) | ||
| Theorem | xnpcan 12995 | Extended real version of npcan 11239. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) | ||
| Theorem | xleadd1a 12996 | Extended real version of leadd1 11452; 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 12997 | Commuted form of xleadd1a 12996. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 +𝑒 𝐴) ≤ (𝐶 +𝑒 𝐵)) | ||
| Theorem | xleadd1 12998 | Weakened version of xleadd1a 12996 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))) | ||
| Theorem | xltadd1 12999 | Extended real version of ltadd1 11451. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶))) | ||
| Theorem | xltadd2 13000 | Extended real version of ltadd2 11088. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 +𝑒 𝐴) < (𝐶 +𝑒 𝐵))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |