Home | Metamath
Proof Explorer Theorem List (p. 121 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | x2times 12001 | Extended real version of 2times 11022. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (2 ·e 𝐴) = (𝐴 +𝑒 𝐴)) | ||
Theorem | xnegcld 12002 | Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → -𝑒𝐴 ∈ ℝ*) | ||
Theorem | xaddcld 12003 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈ ℝ*) | ||
Theorem | xmulcld 12004 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ·e 𝐵) ∈ ℝ*) | ||
Theorem | xadd4d 12005 | Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 10143. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞)) & ⊢ (𝜑 → (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) & ⊢ (𝜑 → (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) & ⊢ (𝜑 → (𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞)) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) | ||
Theorem | xnn0add4d 12006 | Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 12005. (Contributed by AV, 12-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0*) & ⊢ (𝜑 → 𝐵 ∈ ℕ0*) & ⊢ (𝜑 → 𝐶 ∈ ℕ0*) & ⊢ (𝜑 → 𝐷 ∈ ℕ0*) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) | ||
Theorem | xrsupexmnf 12007* | Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005.) |
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {-∞}) ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ (𝐴 ∪ {-∞})𝑦 < 𝑧))) | ||
Theorem | xrinfmexpnf 12008* | Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006.) |
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦))) | ||
Theorem | xrsupsslem 12009* | Lemma for xrsupss 12011. (Contributed by NM, 25-Oct-2005.) |
⊢ ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | xrinfmsslem 12010* | Lemma for xrinfmss 12012. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | xrsupss 12011* | Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005.) |
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | xrinfmss 12012* | Any subset of extended reals has an infimum. (Contributed by NM, 25-Oct-2005.) |
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | xrinfmss2 12013* | Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥◡ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡ < 𝑧))) | ||
Theorem | xrub 12014* | By quantifying only over reals, we can specify any extended real upper bound for any set of extended reals. (Contributed by NM, 9-Apr-2006.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) → (∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) ↔ ∀𝑥 ∈ ℝ* (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) | ||
Theorem | supxr 12015* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) (Revised by Mario Carneiro, 21-Apr-2015.) |
⊢ (((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) → sup(𝐴, ℝ*, < ) = 𝐵) | ||
Theorem | supxr2 12016* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) |
⊢ (((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) → sup(𝐴, ℝ*, < ) = 𝐵) | ||
Theorem | supxrcl 12017 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 24-Oct-2005.) |
⊢ (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | supxrun 12018 | The supremum of the union of two sets of extended reals equals the largest of their suprema. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )) → sup((𝐴 ∪ 𝐵), ℝ*, < ) = sup(𝐵, ℝ*, < )) | ||
Theorem | supxrmnf 12019 | Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∪ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < )) | ||
Theorem | supxrpnf 12020 | The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005.) |
⊢ ((𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴) → sup(𝐴, ℝ*, < ) = +∞) | ||
Theorem | supxrunb1 12021* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞)) | ||
Theorem | supxrunb2 12022* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞)) | ||
Theorem | supxrbnd1 12023* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ sup(𝐴, ℝ*, < ) < +∞)) | ||
Theorem | supxrbnd2 12024* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) < +∞)) | ||
Theorem | xrsup0 12025 | The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005.) |
⊢ sup(∅, ℝ*, < ) = -∞ | ||
Theorem | supxrub 12026 | A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by NM, 7-Feb-2006.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ*, < )) | ||
Theorem | supxrlub 12027* | The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐵 < sup(𝐴, ℝ*, < ) ↔ ∃𝑥 ∈ 𝐴 𝐵 < 𝑥)) | ||
Theorem | supxrleub 12028* | The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006.) (Revised by Mario Carneiro, 6-Sep-2014.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) → (sup(𝐴, ℝ*, < ) ≤ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐵)) | ||
Theorem | supxrre 12029* | The real and extended real suprema match when the real supremum exists. (Contributed by NM, 18-Oct-2005.) (Proof shortened by Mario Carneiro, 7-Sep-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) = sup(𝐴, ℝ, < )) | ||
Theorem | supxrbnd 12030 | The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup(𝐴, ℝ*, < ) < +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ) | ||
Theorem | supxrgtmnf 12031 | The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → -∞ < sup(𝐴, ℝ*, < )) | ||
Theorem | supxrre1 12032 | The supremum of a nonempty set of reals is real iff it is less than plus infinity. (Contributed by NM, 5-Feb-2006.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ sup(𝐴, ℝ*, < ) < +∞)) | ||
Theorem | supxrre2 12033 | The supremum of a nonempty set of reals is real iff it is not plus infinity. (Contributed by NM, 5-Feb-2006.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ sup(𝐴, ℝ*, < ) ≠ +∞)) | ||
Theorem | supxrss 12034 | Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ*) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )) | ||
Theorem | infxrcl 12035 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 19-Jan-2006.) (Revised by AV, 5-Sep-2020.) |
⊢ (𝐴 ⊆ ℝ* → inf(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | infxrlb 12036 | A member of a set of extended reals is greater than or equal to the set's infimum. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 5-Sep-2020.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ≤ 𝐵) | ||
Theorem | infxrgelb 12037* | The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 5-Sep-2020.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐵 ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥)) | ||
Theorem | infxrre 12038* | The real and extended real infima match when the real infimum exists. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 5-Sep-2020.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < )) | ||
Theorem | xrinf0 12039 | The infimum of the empty set under the extended reals is positive infinity. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by AV, 5-Sep-2020.) |
⊢ inf(∅, ℝ*, < ) = +∞ | ||
Theorem | infxrss 12040 | Larger sets of extended reals have smaller infima. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 13-Sep-2020.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ*) → inf(𝐵, ℝ*, < ) ≤ inf(𝐴, ℝ*, < )) | ||
Theorem | reltre 12041* | For all real numbers there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
⊢ ∀𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑦 < 𝑥 | ||
Theorem | rpltrp 12042* | For all positive real numbers there is a smaller positive real number. (Contributed by AV, 5-Sep-2020.) |
⊢ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ 𝑦 < 𝑥 | ||
Theorem | reltxrnmnf 12043* | For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
⊢ ∀𝑥 ∈ ℝ* (-∞ < 𝑥 → ∃𝑦 ∈ ℝ 𝑦 < 𝑥) | ||
Theorem | infmremnf 12044 | The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020.) |
⊢ inf(ℝ, ℝ*, < ) = -∞ | ||
Theorem | infmrp1 12045 | The infimum of the positive reals is 0. (Contributed by AV, 5-Sep-2020.) |
⊢ inf(ℝ+, ℝ, < ) = 0 | ||
Syntax | cioo 12046 | Extend class notation with the set of open intervals of extended reals. |
class (,) | ||
Syntax | cioc 12047 | Extend class notation with the set of open-below, closed-above intervals of extended reals. |
class (,] | ||
Syntax | cico 12048 | Extend class notation with the set of closed-below, open-above intervals of extended reals. |
class [,) | ||
Syntax | cicc 12049 | Extend class notation with the set of closed intervals of extended reals. |
class [,] | ||
Definition | df-ioo 12050* | Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) | ||
Definition | df-ioc 12051* | Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) | ||
Definition | df-ico 12052* | Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | ||
Definition | df-icc 12053* | Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) | ||
Theorem | ixxval 12054* | Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)}) | ||
Theorem | elixx1 12055* | Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴𝑂𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴𝑅𝐶 ∧ 𝐶𝑆𝐵))) | ||
Theorem | ixxf 12056* | The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ 𝑂:(ℝ* × ℝ*)⟶𝒫 ℝ* | ||
Theorem | ixxex 12057* | The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ 𝑂 ∈ V | ||
Theorem | ixxssxr 12058* | The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ ℝ* | ||
Theorem | elixx3g 12059* | Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show 𝐴 ∈ ℝ* and 𝐵 ∈ ℝ*. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ (𝐶 ∈ (𝐴𝑂𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴𝑅𝐶 ∧ 𝐶𝑆𝐵))) | ||
Theorem | ixxssixx 12060* | An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤𝑆𝐵 → 𝑤𝑈𝐵)) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵) | ||
Theorem | ixxdisj 12061* | Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴𝑂𝐵) ∩ (𝐵𝑃𝐶)) = ∅) | ||
Theorem | ixxun 12062* | Split an interval into two parts. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) & ⊢ 𝑄 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑆𝐵 ∧ 𝐵𝑋𝐶) → 𝑤𝑈𝐶)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵 ∧ 𝐵𝑋𝐶)) → ((𝐴𝑂𝐵) ∪ (𝐵𝑃𝐶)) = (𝐴𝑄𝐶)) | ||
Theorem | ixxin 12063* | Intersection of two intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ↔ (𝐴𝑅𝑧 ∧ 𝐶𝑅𝑧))) & ⊢ ((𝑧 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) → (𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷) ↔ (𝑧𝑆𝐵 ∧ 𝑧𝑆𝐷))) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴𝑂𝐵) ∩ (𝐶𝑂𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑂if(𝐵 ≤ 𝐷, 𝐵, 𝐷))) | ||
Theorem | ixxss1 12064* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶)) | ||
Theorem | ixxss2 12065* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑇𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵 ∧ 𝐵𝑊𝐶) → 𝑤𝑆𝐶)) ⇒ ⊢ ((𝐶 ∈ ℝ* ∧ 𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶)) | ||
Theorem | ixxss12 12066* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶 ∧ 𝐶𝑇𝑤) → 𝐴𝑅𝑤)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝑤𝑈𝐷 ∧ 𝐷𝑋𝐵) → 𝑤𝑆𝐵)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵)) | ||
Theorem | ixxub 12067* | Extract the upper bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤𝑆𝐵)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴𝑅𝑤)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ*, < ) = 𝐵) | ||
Theorem | ixxlb 12068* | Extract the lower bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by AV, 12-Sep-2020.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤𝑆𝐵)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴𝑅𝑤)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → inf((𝐴𝑂𝐵), ℝ*, < ) = 𝐴) | ||
Theorem | iooex 12069 | The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (,) ∈ V | ||
Theorem | iooval 12070* | Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | ioo0 12071 | An empty open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | ioon0 12072 | An open interval of extended reals is nonempty iff the lower argument is less than the upper argument. (Contributed by NM, 2-Mar-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) ≠ ∅ ↔ 𝐴 < 𝐵)) | ||
Theorem | ndmioo 12073 | The open interval function's value is empty outside of its domain. (Contributed by NM, 21-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (¬ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = ∅) | ||
Theorem | iooid 12074 | An open interval with identical lower and upper bounds is empty. (Contributed by NM, 21-Jun-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (𝐴(,)𝐴) = ∅ | ||
Theorem | elioo3g 12075 | Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show 𝐴 ∈ ℝ* and 𝐵 ∈ ℝ*. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elioore 12076 | A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ) | ||
Theorem | lbioo 12077 | An open interval does not contain its left endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ¬ 𝐴 ∈ (𝐴(,)𝐵) | ||
Theorem | ubioo 12078 | An open interval does not contain its right endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ¬ 𝐵 ∈ (𝐴(,)𝐵) | ||
Theorem | iooval2 12079* | Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | iooin 12080 | Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)(,)if(𝐵 ≤ 𝐷, 𝐵, 𝐷))) | ||
Theorem | iooss1 12081 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) | ||
Theorem | iooss2 12082 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) | ||
Theorem | iocval 12083* | Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)}) | ||
Theorem | icoval 12084* | Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | iccval 12085* | Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)}) | ||
Theorem | elioo1 12086 | Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elioo2 12087 | Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elioc1 12088 | Membership in an open-below, closed-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | elico1 12089 | Membership in a closed-below, open-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elicc1 12090 | Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | iccid 12091 | A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.) |
⊢ (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴}) | ||
Theorem | ico0 12092 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | ioc0 12093 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴(,]𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | icc0 12094 | An empty closed interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) | ||
Theorem | elicod 12095 | Membership in a left closed, right open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 < 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵)) | ||
Theorem | icogelb 12096 | An element of a left closed right open interval is larger or equal to its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝐶) | ||
Theorem | elicore 12097 | A member of a left closed, right open interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 ∈ ℝ) | ||
Theorem | ubioc1 12098 | The upper bound belongs to an open-below, closed-above interval. See ubicc2 12160. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵)) | ||
Theorem | lbico1 12099 | The lower bound belongs to a closed-below, open-above interval. See lbicc2 12159. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵)) | ||
Theorem | iccleub 12100 | An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |