Home | Metamath
Proof Explorer Theorem List (p. 128 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrsupexmnf 12701* | Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005.) |
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {-∞}) ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ (𝐴 ∪ {-∞})𝑦 < 𝑧))) | ||
Theorem | xrinfmexpnf 12702* | Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006.) |
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦))) | ||
Theorem | xrsupsslem 12703* | Lemma for xrsupss 12705. (Contributed by NM, 25-Oct-2005.) |
⊢ ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | xrinfmsslem 12704* | Lemma for xrinfmss 12706. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | xrsupss 12705* | Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005.) |
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | xrinfmss 12706* | Any subset of extended reals has an infimum. (Contributed by NM, 25-Oct-2005.) |
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | xrinfmss2 12707* | Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥◡ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡ < 𝑧))) | ||
Theorem | xrub 12708* | 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 12709* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) (Revised by Mario Carneiro, 21-Apr-2015.) |
⊢ (((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) → sup(𝐴, ℝ*, < ) = 𝐵) | ||
Theorem | supxr2 12710* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) |
⊢ (((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) → sup(𝐴, ℝ*, < ) = 𝐵) | ||
Theorem | supxrcl 12711 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 24-Oct-2005.) |
⊢ (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | supxrun 12712 | 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 12713 | Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∪ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < )) | ||
Theorem | supxrpnf 12714 | The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005.) |
⊢ ((𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴) → sup(𝐴, ℝ*, < ) = +∞) | ||
Theorem | supxrunb1 12715* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞)) | ||
Theorem | supxrunb2 12716* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞)) | ||
Theorem | supxrbnd1 12717* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ sup(𝐴, ℝ*, < ) < +∞)) | ||
Theorem | supxrbnd2 12718* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) < +∞)) | ||
Theorem | xrsup0 12719 | The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005.) |
⊢ sup(∅, ℝ*, < ) = -∞ | ||
Theorem | supxrub 12720 | 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 12721* | 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 12722* | 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 12723* | 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 12724 | The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup(𝐴, ℝ*, < ) < +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ) | ||
Theorem | supxrgtmnf 12725 | The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → -∞ < sup(𝐴, ℝ*, < )) | ||
Theorem | supxrre1 12726 | 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 12727 | 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 12728 | Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ*) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )) | ||
Theorem | infxrcl 12729 | 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 12730 | 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 12731* | 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 12732* | 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 | infxrmnf 12733 | The infinimum of a set of extended reals containing minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
⊢ ((𝐴 ⊆ ℝ* ∧ -∞ ∈ 𝐴) → inf(𝐴, ℝ*, < ) = -∞) | ||
Theorem | xrinf0 12734 | 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 12735 | 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 12736* | For all real numbers there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
⊢ ∀𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑦 < 𝑥 | ||
Theorem | rpltrp 12737* | For all positive real numbers there is a smaller positive real number. (Contributed by AV, 5-Sep-2020.) |
⊢ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ 𝑦 < 𝑥 | ||
Theorem | reltxrnmnf 12738* | For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
⊢ ∀𝑥 ∈ ℝ* (-∞ < 𝑥 → ∃𝑦 ∈ ℝ 𝑦 < 𝑥) | ||
Theorem | infmremnf 12739 | The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020.) |
⊢ inf(ℝ, ℝ*, < ) = -∞ | ||
Theorem | infmrp1 12740 | The infimum of the positive reals is 0. (Contributed by AV, 5-Sep-2020.) |
⊢ inf(ℝ+, ℝ, < ) = 0 | ||
Syntax | cioo 12741 | Extend class notation with the set of open intervals of extended reals. |
class (,) | ||
Syntax | cioc 12742 | Extend class notation with the set of open-below, closed-above intervals of extended reals. |
class (,] | ||
Syntax | cico 12743 | Extend class notation with the set of closed-below, open-above intervals of extended reals. |
class [,) | ||
Syntax | cicc 12744 | Extend class notation with the set of closed intervals of extended reals. |
class [,] | ||
Definition | df-ioo 12745* | Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) | ||
Definition | df-ioc 12746* | Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) | ||
Definition | df-ico 12747* | Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | ||
Definition | df-icc 12748* | Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) | ||
Theorem | ixxval 12749* | Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)}) | ||
Theorem | elixx1 12750* | Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴𝑂𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴𝑅𝐶 ∧ 𝐶𝑆𝐵))) | ||
Theorem | ixxf 12751* | 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 12752* | 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 12753* | The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ ℝ* | ||
Theorem | elixx3g 12754* | 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 12755* | An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤𝑆𝐵 → 𝑤𝑈𝐵)) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵) | ||
Theorem | ixxdisj 12756* | Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴𝑂𝐵) ∩ (𝐵𝑃𝐶)) = ∅) | ||
Theorem | ixxun 12757* | Split an interval into two parts. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) & ⊢ 𝑄 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑆𝐵 ∧ 𝐵𝑋𝐶) → 𝑤𝑈𝐶)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵 ∧ 𝐵𝑋𝐶)) → ((𝐴𝑂𝐵) ∪ (𝐵𝑃𝐶)) = (𝐴𝑄𝐶)) | ||
Theorem | ixxin 12758* | Intersection of two intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ↔ (𝐴𝑅𝑧 ∧ 𝐶𝑅𝑧))) & ⊢ ((𝑧 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) → (𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷) ↔ (𝑧𝑆𝐵 ∧ 𝑧𝑆𝐷))) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴𝑂𝐵) ∩ (𝐶𝑂𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑂if(𝐵 ≤ 𝐷, 𝐵, 𝐷))) | ||
Theorem | ixxss1 12759* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶)) | ||
Theorem | ixxss2 12760* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑇𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵 ∧ 𝐵𝑊𝐶) → 𝑤𝑆𝐶)) ⇒ ⊢ ((𝐶 ∈ ℝ* ∧ 𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶)) | ||
Theorem | ixxss12 12761* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶 ∧ 𝐶𝑇𝑤) → 𝐴𝑅𝑤)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝑤𝑈𝐷 ∧ 𝐷𝑋𝐵) → 𝑤𝑆𝐵)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵)) | ||
Theorem | ixxub 12762* | Extract the upper bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤𝑆𝐵)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴𝑅𝑤)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ*, < ) = 𝐵) | ||
Theorem | ixxlb 12763* | Extract the lower bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by AV, 12-Sep-2020.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤𝑆𝐵)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴𝑅𝑤)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → inf((𝐴𝑂𝐵), ℝ*, < ) = 𝐴) | ||
Theorem | iooex 12764 | 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 12765* | Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | ioo0 12766 | An empty open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | ioon0 12767 | 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 12768 | 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 12769 | 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 12770 | 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 12771 | 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 12772 | An open interval does not contain its left endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ¬ 𝐴 ∈ (𝐴(,)𝐵) | ||
Theorem | ubioo 12773 | An open interval does not contain its right endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ¬ 𝐵 ∈ (𝐴(,)𝐵) | ||
Theorem | iooval2 12774* | Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | iooin 12775 | 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 12776 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) | ||
Theorem | iooss2 12777 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) | ||
Theorem | iocval 12778* | Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)}) | ||
Theorem | icoval 12779* | Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | iccval 12780* | Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)}) | ||
Theorem | elioo1 12781 | Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elioo2 12782 | Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elioc1 12783 | 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 12784 | 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 12785 | Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | iccid 12786 | A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.) |
⊢ (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴}) | ||
Theorem | ico0 12787 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | ioc0 12788 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴(,]𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | icc0 12789 | An empty closed interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) | ||
Theorem | elicod 12790 | Membership in a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 < 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵)) | ||
Theorem | icogelb 12791 | An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝐶) | ||
Theorem | elicore 12792 | A member of a left-closed right-open interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 ∈ ℝ) | ||
Theorem | ubioc1 12793 | The upper bound belongs to an open-below, closed-above interval. See ubicc2 12856. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵)) | ||
Theorem | lbico1 12794 | The lower bound belongs to a closed-below, open-above interval. See lbicc2 12855. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵)) | ||
Theorem | iccleub 12795 | An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵) | ||
Theorem | iccgelb 12796 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) | ||
Theorem | elioo5 12797 | Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | eliooxr 12798 | A nonempty open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*)) | ||
Theorem | eliooord 12799 | Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) | ||
Theorem | elioo4g 12800 | Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |