HomeTheorem List (p. 133 of 507)
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. 133 of 507) | < 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-31300) |
Hilbert Space Explorer
(31301-32823) |
Users' Mathboxes
(32824-50686) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | xrletr 13201 | Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) | ||
| Theorem | xrlttrd 13202 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | xrlelttrd 13203 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | xrltletrd 13204 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
| Theorem | xrletrd 13205 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) | ||
| Theorem | xrltne 13206 | 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) | ||
| Theorem | xrgtned 13207 | 'Greater than' implies not equal. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) | ||
| Theorem | nltpnft 13208 | An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) | ||
| Theorem | xgepnf 13209 | An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
| ⊢ (𝐴 ∈ ℝ* → (+∞ ≤ 𝐴 ↔ 𝐴 = +∞)) | ||
| Theorem | ngtmnft 13210 | An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴)) | ||
| Theorem | xlemnf 13211 | An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ -∞ ↔ 𝐴 = -∞)) | ||
| Theorem | xrrebnd 13212 | An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴 ∧ 𝐴 < +∞))) | ||
| Theorem | xrre 13213 | A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) | ||
| Theorem | xrre2 13214 | An extended real between two others is real. (Contributed by NM, 6-Feb-2007.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ) | ||
| Theorem | xrre3 13215 | A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < +∞)) → 𝐴 ∈ ℝ) | ||
| Theorem | ge0gtmnf 13216 | A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → -∞ < 𝐴) | ||
| Theorem | ge0nemnf 13217 | A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≠ -∞) | ||
| Theorem | xrrege0 13218 | A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) | ||
| Theorem | xrmax1 13219 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | xrmax2 13220 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | xrmin1 13221 | The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴) | ||
| Theorem | xrmin2 13222 | The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵) | ||
| Theorem | xrmaxeq 13223 | 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 13224 | 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 13225 | Two ways of saying the maximum of two extended reals is less than a third. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) | ||
| Theorem | xrltmin 13226 | Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶))) | ||
| Theorem | xrmaxle 13227 | 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 13228 | 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 13229 | A number is less than or equal to the maximum of it and another. See also max1ALT 13230. (Contributed by NM, 3-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | max1ALT 13230 | A number is less than or equal to the maximum of it and another. This version of max1 13229 omits the 𝐵 ∈ ℝ antecedent. Although it doesn't exploit undefined behavior, it is still considered poor style, and the use of max1 13229 is preferred. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 3-Apr-2005.) |
| ⊢ (𝐴 ∈ ℝ → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | max2 13231 | A number is less than or equal to the maximum of it and another. (Contributed by NM, 3-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | 2resupmax 13232 | The supremum of two real numbers is the maximum of these two numbers. (Contributed by AV, 8-Jun-2021.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
| Theorem | min1 13233 | The minimum of two numbers is less than or equal to the first. (Contributed by NM, 3-Aug-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴) | ||
| Theorem | min2 13234 | The minimum of two numbers is less than or equal to the second. (Contributed by NM, 3-Aug-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵) | ||
| Theorem | maxle 13235 | 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 13236 | 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 13237 | Two ways of saying the maximum of two numbers is less than a third. (Contributed by NM, 3-Aug-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) | ||
| Theorem | ltmin 13238 | Two ways of saying a number is less than the minimum of two others. (Contributed by NM, 1-Sep-2006.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶))) | ||
| Theorem | lemaxle 13239 | 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 13240 | Decompose a real number into positive and negative parts. (Contributed by Mario Carneiro, 6-Aug-2014.) |
| ⊢ (𝐴 ∈ ℝ → (if(0 ≤ 𝐴, 𝐴, 0) − if(0 ≤ -𝐴, -𝐴, 0)) = 𝐴) | ||
| Theorem | ifle 13241 | An if statement transforms an implication into an inequality of terms. (Contributed by Mario Carneiro, 31-Aug-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≤ 𝐴) ∧ (𝜑 → 𝜓)) → if(𝜑, 𝐴, 𝐵) ≤ if(𝜓, 𝐴, 𝐵)) | ||
| Theorem | z2ge 13242* | There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘)) | ||
| Theorem | qbtwnre 13243* | 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 13244* | 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 13245* | If a nonnegative real is less than any positive rational, it is zero. (Contributed by NM, 6-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℚ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0) | ||
| Theorem | qextltlem 13246* | Lemma for qextlt 13247 and qextle . (Contributed by Mario Carneiro, 3-Oct-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))) | ||
| Theorem | qextlt 13247* | An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵))) | ||
| Theorem | qextle 13248* | An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵))) | ||
| Theorem | xralrple 13249* | 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 13250* | 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 13251 | 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 13252 | A negative extended real exists as a set. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ -𝑒𝐴 ∈ V | ||
| Theorem | xnegpnf 13253 | Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) |
| ⊢ -𝑒+∞ = -∞ | ||
| Theorem | xnegmnf 13254 | Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.) |
| ⊢ -𝑒-∞ = +∞ | ||
| Theorem | rexneg 13255 | 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 13256 | The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ -𝑒0 = 0 | ||
| Theorem | xnegcl 13257 | Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*) | ||
| Theorem | xnegneg 13258 | Extended real version of negneg 11526. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴) | ||
| Theorem | xneg11 13259 | Extended real version of neg11 11527. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | xltnegi 13260 | Forward direction of xltneg 13261. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴) | ||
| Theorem | xltneg 13261 | Extended real version of ltneg 11732. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴)) | ||
| Theorem | xleneg 13262 | Extended real version of leneg 11735. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴)) | ||
| Theorem | xlt0neg1 13263 | Extended real version of lt0neg1 11738. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴)) | ||
| Theorem | xlt0neg2 13264 | Extended real version of lt0neg2 11739. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (0 < 𝐴 ↔ -𝑒𝐴 < 0)) | ||
| Theorem | xle0neg1 13265 | Extended real version of le0neg1 11740. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤ -𝑒𝐴)) | ||
| Theorem | xle0neg2 13266 | Extended real version of le0neg2 11741. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (0 ≤ 𝐴 ↔ -𝑒𝐴 ≤ 0)) | ||
| Theorem | xaddval 13267 | Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = if(𝐴 = +∞, if(𝐵 = -∞, 0, +∞), if(𝐴 = -∞, if(𝐵 = +∞, 0, -∞), if(𝐵 = +∞, +∞, if(𝐵 = -∞, -∞, (𝐴 + 𝐵)))))) | ||
| Theorem | xaddf 13268 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ +𝑒 :(ℝ* × ℝ*)⟶ℝ* | ||
| Theorem | xmulval 13269 | 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 13270 | Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞) | ||
| Theorem | xaddpnf2 13271 | Addition of positive infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (+∞ +𝑒 𝐴) = +∞) | ||
| Theorem | xaddmnf1 13272 | Addition of negative infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞) | ||
| Theorem | xaddmnf2 13273 | Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (-∞ +𝑒 𝐴) = -∞) | ||
| Theorem | pnfaddmnf 13274 | 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 13275 | 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 13276 | The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) | ||
| Theorem | rexsub 13277 | Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 -𝑒𝐵) = (𝐴 − 𝐵)) | ||
| Theorem | rexaddd 13278 | The extended real addition operation when both arguments are real. Deduction version of rexadd 13276. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) | ||
| Theorem | xnn0xaddcl 13279 | The extended nonnegative integers are closed under extended addition. (Contributed by AV, 10-Dec-2020.) |
| ⊢ ((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → (𝐴 +𝑒 𝐵) ∈ ℕ0*) | ||
| Theorem | xaddnemnf 13280 | Closure of extended real addition in the subset ℝ* / {-∞}. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) → (𝐴 +𝑒 𝐵) ≠ -∞) | ||
| Theorem | xaddnepnf 13281 | Closure of extended real addition in the subset ℝ* / {+∞}. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞)) → (𝐴 +𝑒 𝐵) ≠ +∞) | ||
| Theorem | xnegid 13282 | Extended real version of negid 11523. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 -𝑒𝐴) = 0) | ||
| Theorem | xaddcl 13283 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*) | ||
| Theorem | xaddcom 13284 | The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | ||
| Theorem | xaddrid 13285 | Extended real version of addrid 11408. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 0) = 𝐴) | ||
| Theorem | xaddlid 13286 | Extended real version of addlid 11411. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (𝐴 ∈ ℝ* → (0 +𝑒 𝐴) = 𝐴) | ||
| Theorem | xaddridd 13287 | 0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 0) = 𝐴) | ||
| Theorem | xnn0lem1lt 13288 | Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0*) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) | ||
| Theorem | xnn0lenn0nn0 13289 | 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 13290 | 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 13291 | 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 13292 | Extended real version of negdi 11533. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵)) | ||
| Theorem | xaddass 13293 | 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 13294, where +∞ is not present. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
| Theorem | xaddass2 13294 | Associativity of extended real addition. See xaddass 13293 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
| Theorem | xpncan 13295 | Extended real version of pncan 11481. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 -𝑒𝐵) = 𝐴) | ||
| Theorem | xnpcan 13296 | Extended real version of npcan 11484. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) | ||
| Theorem | xleadd1a 13297 | Extended real version of leadd1 11700; 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 13298 | Commuted form of xleadd1a 13297. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 +𝑒 𝐴) ≤ (𝐶 +𝑒 𝐵)) | ||
| Theorem | xleadd1 13299 | Weakened version of xleadd1a 13297 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))) | ||
| Theorem | xltadd1 13300 | Extended real version of ltadd1 11699. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |