![]() |
Metamath
Proof Explorer Theorem List (p. 126 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrnepnf 12501 | An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = -∞)) | ||
Theorem | xrltnr 12502 | The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.) |
⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴) | ||
Theorem | ltpnf 12503 | Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.) |
⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) | ||
Theorem | ltpnfd 12504 | Any (finite) real is less than plus infinity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 < +∞) | ||
Theorem | 0ltpnf 12505 | Zero is less than plus infinity. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 < +∞ | ||
Theorem | mnflt 12506 | Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.) |
⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) | ||
Theorem | mnfltd 12507 | Minus infinity is less than any (finite) real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → -∞ < 𝐴) | ||
Theorem | mnflt0 12508 | Minus infinity is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -∞ < 0 | ||
Theorem | mnfltpnf 12509 | Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.) |
⊢ -∞ < +∞ | ||
Theorem | mnfltxr 12510 | Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.) |
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴) | ||
Theorem | pnfnlt 12511 | No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.) |
⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴) | ||
Theorem | nltmnf 12512 | No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.) |
⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < -∞) | ||
Theorem | pnfge 12513 | Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞) | ||
Theorem | xnn0n0n1ge2b 12514 | An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by AV, 5-Apr-2021.) |
⊢ (𝑁 ∈ ℕ0* → ((𝑁 ≠ 0 ∧ 𝑁 ≠ 1) ↔ 2 ≤ 𝑁)) | ||
Theorem | 0lepnf 12515 | 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ≤ +∞ | ||
Theorem | xnn0ge0 12516 | An extended nonnegative integer is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 10-Dec-2020.) |
⊢ (𝑁 ∈ ℕ0* → 0 ≤ 𝑁) | ||
Theorem | mnfle 12517 | Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ∈ ℝ* → -∞ ≤ 𝐴) | ||
Theorem | xrltnsym 12518 | Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) | ||
Theorem | xrltnsym2 12519 | 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) | ||
Theorem | xrlttri 12520 | Ordering on the extended reals satisfies strict trichotomy. New proofs should generally use this instead of ax-pre-lttri 10600 or axlttri 10701. (Contributed by NM, 14-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))) | ||
Theorem | xrlttr 12521 | Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
Theorem | xrltso 12522 | 'Less than' is a strict ordering on the extended reals. (Contributed by NM, 15-Oct-2005.) |
⊢ < Or ℝ* | ||
Theorem | xrlttri2 12523 | Trichotomy law for 'less than' for extended reals. (Contributed by NM, 10-Dec-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
Theorem | xrlttri3 12524 | Trichotomy law for 'less than' for extended reals. (Contributed by NM, 9-Feb-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) | ||
Theorem | xrleloe 12525 | 'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | xrleltne 12526 | 'Less than or equal to' implies 'less than' is not 'equals', for extended reals. (Contributed by NM, 9-Feb-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴)) | ||
Theorem | xrltlen 12527 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) | ||
Theorem | dfle2 12528 | Alternative definition of 'less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
⊢ ≤ = ( < ∪ ( I ↾ ℝ*)) | ||
Theorem | dflt2 12529 | Alternative definition of 'less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
⊢ < = ( ≤ ∖ I ) | ||
Theorem | xrltle 12530 | 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) | ||
Theorem | xrltled 12531 | 'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 12530. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | xrleid 12532 | 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.) |
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴) | ||
Theorem | xrleidd 12533 | 'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 12532. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐴) | ||
Theorem | xrletri 12534 | Trichotomy law for extended reals. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) | ||
Theorem | xrletri3 12535 | Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) | ||
Theorem | xrletrid 12536 | Trichotomy law for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | xrlelttr 12537 | Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
Theorem | xrltletr 12538 | Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) | ||
Theorem | xrletr 12539 | Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) | ||
Theorem | xrlttrd 12540 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
Theorem | xrlelttrd 12541 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
Theorem | xrltletrd 12542 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
Theorem | xrletrd 12543 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) | ||
Theorem | xrltne 12544 | 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) | ||
Theorem | nltpnft 12545 | An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) | ||
Theorem | xgepnf 12546 | An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝐴 ∈ ℝ* → (+∞ ≤ 𝐴 ↔ 𝐴 = +∞)) | ||
Theorem | ngtmnft 12547 | An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴)) | ||
Theorem | xlemnf 12548 | An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ -∞ ↔ 𝐴 = -∞)) | ||
Theorem | xrrebnd 12549 | An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴 ∧ 𝐴 < +∞))) | ||
Theorem | xrre 12550 | A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) | ||
Theorem | xrre2 12551 | An extended real between two others is real. (Contributed by NM, 6-Feb-2007.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ) | ||
Theorem | xrre3 12552 | A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < +∞)) → 𝐴 ∈ ℝ) | ||
Theorem | ge0gtmnf 12553 | A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → -∞ < 𝐴) | ||
Theorem | ge0nemnf 12554 | A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≠ -∞) | ||
Theorem | xrrege0 12555 | A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) | ||
Theorem | xrmax1 12556 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | xrmax2 12557 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | xrmin1 12558 | The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴) | ||
Theorem | xrmin2 12559 | The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵) | ||
Theorem | xrmaxeq 12560 | 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 12561 | 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 12562 | Two ways of saying the maximum of two extended reals is less than a third. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) | ||
Theorem | xrltmin 12563 | Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶))) | ||
Theorem | xrmaxle 12564 | 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 12565 | 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 12566 | A number is less than or equal to the maximum of it and another. See also max1ALT 12567. (Contributed by NM, 3-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | max1ALT 12567 | A number is less than or equal to the maximum of it and another. This version of max1 12566 omits the 𝐵 ∈ ℝ antecedent. Although it doesn't exploit undefined behavior, it is still considered poor style, and the use of max1 12566 is preferred. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 3-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | max2 12568 | A number is less than or equal to the maximum of it and another. (Contributed by NM, 3-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | 2resupmax 12569 | The supremum of two real numbers is the maximum of these two numbers. (Contributed by AV, 8-Jun-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | min1 12570 | The minimum of two numbers is less than or equal to the first. (Contributed by NM, 3-Aug-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴) | ||
Theorem | min2 12571 | The minimum of two numbers is less than or equal to the second. (Contributed by NM, 3-Aug-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵) | ||
Theorem | maxle 12572 | 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 12573 | 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 12574 | Two ways of saying the maximum of two numbers is less than a third. (Contributed by NM, 3-Aug-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) | ||
Theorem | ltmin 12575 | Two ways of saying a number is less than the minimum of two others. (Contributed by NM, 1-Sep-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶))) | ||
Theorem | lemaxle 12576 | 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 12577 | Decompose a real number into positive and negative parts. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ (𝐴 ∈ ℝ → (if(0 ≤ 𝐴, 𝐴, 0) − if(0 ≤ -𝐴, -𝐴, 0)) = 𝐴) | ||
Theorem | ifle 12578 | An if statement transforms an implication into an inequality of terms. (Contributed by Mario Carneiro, 31-Aug-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≤ 𝐴) ∧ (𝜑 → 𝜓)) → if(𝜑, 𝐴, 𝐵) ≤ if(𝜓, 𝐴, 𝐵)) | ||
Theorem | z2ge 12579* | There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘)) | ||
Theorem | qbtwnre 12580* | 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 12581* | 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 12582* | If a nonnegative real is less than any positive rational, it is zero. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℚ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0) | ||
Theorem | qextltlem 12583* | Lemma for qextlt 12584 and qextle . (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))) | ||
Theorem | qextlt 12584* | An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵))) | ||
Theorem | qextle 12585* | An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵))) | ||
Theorem | xralrple 12586* | 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 12587* | 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 12588 | 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 12589 | A negative extended real exists as a set. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ -𝑒𝐴 ∈ V | ||
Theorem | xnegpnf 12590 | Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) |
⊢ -𝑒+∞ = -∞ | ||
Theorem | xnegmnf 12591 | Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.) |
⊢ -𝑒-∞ = +∞ | ||
Theorem | rexneg 12592 | 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 12593 | The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ -𝑒0 = 0 | ||
Theorem | xnegcl 12594 | Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*) | ||
Theorem | xnegneg 12595 | Extended real version of negneg 10925. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴) | ||
Theorem | xneg11 12596 | Extended real version of neg11 10926. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | xltnegi 12597 | Forward direction of xltneg 12598. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴) | ||
Theorem | xltneg 12598 | Extended real version of ltneg 11129. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴)) | ||
Theorem | xleneg 12599 | Extended real version of leneg 11132. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴)) | ||
Theorem | xlt0neg1 12600 | Extended real version of lt0neg1 11135. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |