![]() |
Metamath
Proof Explorer Theorem List (p. 132 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ltpnfd 13101 | Any (finite) real is less than plus infinity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 < +∞) | ||
Theorem | 0ltpnf 13102 | Zero is less than plus infinity. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 < +∞ | ||
Theorem | mnflt 13103 | Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.) |
⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) | ||
Theorem | mnfltd 13104 | Minus infinity is less than any (finite) real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → -∞ < 𝐴) | ||
Theorem | mnflt0 13105 | Minus infinity is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -∞ < 0 | ||
Theorem | mnfltpnf 13106 | Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.) |
⊢ -∞ < +∞ | ||
Theorem | mnfltxr 13107 | Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.) |
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴) | ||
Theorem | pnfnlt 13108 | No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.) |
⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴) | ||
Theorem | nltmnf 13109 | No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.) |
⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < -∞) | ||
Theorem | pnfge 13110 | Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞) | ||
Theorem | xnn0n0n1ge2b 13111 | 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 13112 | 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ≤ +∞ | ||
Theorem | xnn0ge0 13113 | 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 13114 | Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ∈ ℝ* → -∞ ≤ 𝐴) | ||
Theorem | mnfled 13115 | Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → -∞ ≤ 𝐴) | ||
Theorem | xrltnsym 13116 | Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) | ||
Theorem | xrltnsym2 13117 | 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) | ||
Theorem | xrlttri 13118 | Ordering on the extended reals satisfies strict trichotomy. New proofs should generally use this instead of ax-pre-lttri 11184 or axlttri 11285. (Contributed by NM, 14-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴))) | ||
Theorem | xrlttr 13119 | Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
Theorem | xrltso 13120 | 'Less than' is a strict ordering on the extended reals. (Contributed by NM, 15-Oct-2005.) |
⊢ < Or ℝ* | ||
Theorem | xrlttri2 13121 | Trichotomy law for 'less than' for extended reals. (Contributed by NM, 10-Dec-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
Theorem | xrlttri3 13122 | Trichotomy law for 'less than' for extended reals. (Contributed by NM, 9-Feb-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) | ||
Theorem | xrleloe 13123 | 'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | xrleltne 13124 | 'Less than or equal to' implies 'less than' is not 'equals', for extended reals. (Contributed by NM, 9-Feb-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴)) | ||
Theorem | xrltlen 13125 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴))) | ||
Theorem | dfle2 13126 | Alternative definition of 'less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
⊢ ≤ = ( < ∪ ( I ↾ ℝ*)) | ||
Theorem | dflt2 13127 | Alternative definition of 'less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
⊢ < = ( ≤ ∖ I ) | ||
Theorem | xrltle 13128 | 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) | ||
Theorem | xrltled 13129 | 'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 13128. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | xrleid 13130 | 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.) |
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴) | ||
Theorem | xrleidd 13131 | 'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 13130. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐴) | ||
Theorem | xrletri 13132 | Trichotomy law for extended reals. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) | ||
Theorem | xrletri3 13133 | Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) | ||
Theorem | xrletrid 13134 | Trichotomy law for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | xrlelttr 13135 | Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | ||
Theorem | xrltletr 13136 | Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) | ||
Theorem | xrletr 13137 | Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) | ||
Theorem | xrlttrd 13138 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
Theorem | xrlelttrd 13139 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
Theorem | xrltletrd 13140 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
Theorem | xrletrd 13141 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) | ||
Theorem | xrltne 13142 | 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) | ||
Theorem | nltpnft 13143 | An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) | ||
Theorem | xgepnf 13144 | An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
⊢ (𝐴 ∈ ℝ* → (+∞ ≤ 𝐴 ↔ 𝐴 = +∞)) | ||
Theorem | ngtmnft 13145 | An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴)) | ||
Theorem | xlemnf 13146 | An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ -∞ ↔ 𝐴 = -∞)) | ||
Theorem | xrrebnd 13147 | An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴 ∧ 𝐴 < +∞))) | ||
Theorem | xrre 13148 | A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) | ||
Theorem | xrre2 13149 | An extended real between two others is real. (Contributed by NM, 6-Feb-2007.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ) | ||
Theorem | xrre3 13150 | A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < +∞)) → 𝐴 ∈ ℝ) | ||
Theorem | ge0gtmnf 13151 | A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → -∞ < 𝐴) | ||
Theorem | ge0nemnf 13152 | A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≠ -∞) | ||
Theorem | xrrege0 13153 | A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) | ||
Theorem | xrmax1 13154 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | xrmax2 13155 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | xrmin1 13156 | The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴) | ||
Theorem | xrmin2 13157 | The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵) | ||
Theorem | xrmaxeq 13158 | 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 13159 | 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 13160 | Two ways of saying the maximum of two extended reals is less than a third. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) | ||
Theorem | xrltmin 13161 | Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶))) | ||
Theorem | xrmaxle 13162 | 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 13163 | 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 13164 | A number is less than or equal to the maximum of it and another. See also max1ALT 13165. (Contributed by NM, 3-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | max1ALT 13165 | A number is less than or equal to the maximum of it and another. This version of max1 13164 omits the 𝐵 ∈ ℝ antecedent. Although it doesn't exploit undefined behavior, it is still considered poor style, and the use of max1 13164 is preferred. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 3-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | max2 13166 | A number is less than or equal to the maximum of it and another. (Contributed by NM, 3-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | 2resupmax 13167 | The supremum of two real numbers is the maximum of these two numbers. (Contributed by AV, 8-Jun-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | min1 13168 | The minimum of two numbers is less than or equal to the first. (Contributed by NM, 3-Aug-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴) | ||
Theorem | min2 13169 | The minimum of two numbers is less than or equal to the second. (Contributed by NM, 3-Aug-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵) | ||
Theorem | maxle 13170 | 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 13171 | 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 13172 | Two ways of saying the maximum of two numbers is less than a third. (Contributed by NM, 3-Aug-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶))) | ||
Theorem | ltmin 13173 | Two ways of saying a number is less than the minimum of two others. (Contributed by NM, 1-Sep-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶))) | ||
Theorem | lemaxle 13174 | 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 13175 | Decompose a real number into positive and negative parts. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ (𝐴 ∈ ℝ → (if(0 ≤ 𝐴, 𝐴, 0) − if(0 ≤ -𝐴, -𝐴, 0)) = 𝐴) | ||
Theorem | ifle 13176 | An if statement transforms an implication into an inequality of terms. (Contributed by Mario Carneiro, 31-Aug-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≤ 𝐴) ∧ (𝜑 → 𝜓)) → if(𝜑, 𝐴, 𝐵) ≤ if(𝜓, 𝐴, 𝐵)) | ||
Theorem | z2ge 13177* | There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘)) | ||
Theorem | qbtwnre 13178* | 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 13179* | 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 13180* | If a nonnegative real is less than any positive rational, it is zero. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℚ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0) | ||
Theorem | qextltlem 13181* | Lemma for qextlt 13182 and qextle . (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))) | ||
Theorem | qextlt 13182* | An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵))) | ||
Theorem | qextle 13183* | An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵))) | ||
Theorem | xralrple 13184* | 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 13185* | 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 13186 | 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 13187 | A negative extended real exists as a set. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ -𝑒𝐴 ∈ V | ||
Theorem | xnegpnf 13188 | Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) |
⊢ -𝑒+∞ = -∞ | ||
Theorem | xnegmnf 13189 | Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.) |
⊢ -𝑒-∞ = +∞ | ||
Theorem | rexneg 13190 | 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 13191 | The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ -𝑒0 = 0 | ||
Theorem | xnegcl 13192 | Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*) | ||
Theorem | xnegneg 13193 | Extended real version of negneg 11510. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴) | ||
Theorem | xneg11 13194 | Extended real version of neg11 11511. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | xltnegi 13195 | Forward direction of xltneg 13196. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴) | ||
Theorem | xltneg 13196 | Extended real version of ltneg 11714. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴)) | ||
Theorem | xleneg 13197 | Extended real version of leneg 11717. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴)) | ||
Theorem | xlt0neg1 13198 | Extended real version of lt0neg1 11720. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴)) | ||
Theorem | xlt0neg2 13199 | Extended real version of lt0neg2 11721. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (0 < 𝐴 ↔ -𝑒𝐴 < 0)) | ||
Theorem | xle0neg1 13200 | Extended real version of le0neg1 11722. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤ -𝑒𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |