![]() |
Metamath
Proof Explorer Theorem List (p. 126 of 437) | < 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-28361) |
![]() (28362-29886) |
![]() (29887-43649) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ixxssixx 12501* | An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴𝑅𝑤 → 𝐴𝑇𝑤)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤𝑆𝐵 → 𝑤𝑈𝐵)) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ (𝐴𝑃𝐵) | ||
Theorem | ixxdisj 12502* | Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴𝑂𝐵) ∩ (𝐵𝑃𝐶)) = ∅) | ||
Theorem | ixxun 12503* | Split an interval into two parts. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐵𝑇𝑤 ↔ ¬ 𝑤𝑆𝐵)) & ⊢ 𝑄 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑆𝐵 ∧ 𝐵𝑋𝐶) → 𝑤𝑈𝐶)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴𝑊𝐵 ∧ 𝐵𝑋𝐶)) → ((𝐴𝑂𝐵) ∪ (𝐵𝑃𝐶)) = (𝐴𝑄𝐶)) | ||
Theorem | ixxin 12504* | Intersection of two intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑅𝑧 ↔ (𝐴𝑅𝑧 ∧ 𝐶𝑅𝑧))) & ⊢ ((𝑧 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) → (𝑧𝑆if(𝐵 ≤ 𝐷, 𝐵, 𝐷) ↔ (𝑧𝑆𝐵 ∧ 𝑧𝑆𝐷))) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴𝑂𝐵) ∩ (𝐶𝑂𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)𝑂if(𝐵 ≤ 𝐷, 𝐵, 𝐷))) | ||
Theorem | ixxss1 12505* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐵 ∧ 𝐵𝑇𝑤) → 𝐴𝑅𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴𝑊𝐵) → (𝐵𝑃𝐶) ⊆ (𝐴𝑂𝐶)) | ||
Theorem | ixxss2 12506* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑇𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵 ∧ 𝐵𝑊𝐶) → 𝑤𝑆𝐶)) ⇒ ⊢ ((𝐶 ∈ ℝ* ∧ 𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶)) | ||
Theorem | ixxss12 12507* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧 ∧ 𝑧𝑈𝑦)}) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶 ∧ 𝐶𝑇𝑤) → 𝐴𝑅𝑤)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝑤𝑈𝐷 ∧ 𝐷𝑋𝐵) → 𝑤𝑆𝐵)) ⇒ ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶 ∧ 𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵)) | ||
Theorem | ixxub 12508* | Extract the upper bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤𝑆𝐵)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴𝑅𝑤)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → sup((𝐴𝑂𝐵), ℝ*, < ) = 𝐵) | ||
Theorem | ixxlb 12509* | Extract the lower bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by AV, 12-Sep-2020.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤𝑆𝐵)) & ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤𝑆𝐵 → 𝑤 ≤ 𝐵)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴𝑅𝑤)) & ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴𝑅𝑤 → 𝐴 ≤ 𝑤)) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐴𝑂𝐵) ≠ ∅) → inf((𝐴𝑂𝐵), ℝ*, < ) = 𝐴) | ||
Theorem | iooex 12510 | 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 12511* | Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | ioo0 12512 | An empty open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | ioon0 12513 | 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 12514 | 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 12515 | 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 12516 | 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 12517 | 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 12518 | An open interval does not contain its left endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ¬ 𝐴 ∈ (𝐴(,)𝐵) | ||
Theorem | ubioo 12519 | An open interval does not contain its right endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ¬ 𝐵 ∈ (𝐴(,)𝐵) | ||
Theorem | iooval2 12520* | Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | iooin 12521 | 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 12522 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) | ||
Theorem | iooss2 12523 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) | ||
Theorem | iocval 12524* | Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)}) | ||
Theorem | icoval 12525* | Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | iccval 12526* | Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)}) | ||
Theorem | elioo1 12527 | Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elioo2 12528 | Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elioc1 12529 | 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 12530 | 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 12531 | Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | iccid 12532 | A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.) |
⊢ (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴}) | ||
Theorem | ico0 12533 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | ioc0 12534 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴(,]𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | icc0 12535 | An empty closed interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) | ||
Theorem | elicod 12536 | Membership in a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 < 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵)) | ||
Theorem | icogelb 12537 | 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 12538 | A member of a left-closed right-open interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 ∈ ℝ) | ||
Theorem | ubioc1 12539 | The upper bound belongs to an open-below, closed-above interval. See ubicc2 12603. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵)) | ||
Theorem | lbico1 12540 | The lower bound belongs to a closed-below, open-above interval. See lbicc2 12602. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵)) | ||
Theorem | iccleub 12541 | An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵) | ||
Theorem | iccgelb 12542 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) | ||
Theorem | elioo5 12543 | Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | eliooxr 12544 | A nonempty open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*)) | ||
Theorem | eliooord 12545 | 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 12546 | Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | ioossre 12547 | An open interval is a set of reals. (Contributed by NM, 31-May-2007.) |
⊢ (𝐴(,)𝐵) ⊆ ℝ | ||
Theorem | elioc2 12548 | Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | elico2 12549 | Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elicc2 12550 | Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | elicc2i 12551 | Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) | ||
Theorem | elicc4 12552 | Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | iccss 12553 | Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 20-Feb-2015.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,]𝐵)) | ||
Theorem | iccssioo 12554 | Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | icossico 12555 | Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴[,)𝐵)) | ||
Theorem | iccss2 12556 | Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐷 ∈ (𝐴[,]𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,]𝐵)) | ||
Theorem | iccssico 12557 | Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,)𝐵)) | ||
Theorem | iccssioo2 12558 | Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
⊢ ((𝐶 ∈ (𝐴(,)𝐵) ∧ 𝐷 ∈ (𝐴(,)𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | iccssico2 12559 | Condition for a closed interval to be a subset of a closed-below, open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
⊢ ((𝐶 ∈ (𝐴[,)𝐵) ∧ 𝐷 ∈ (𝐴[,)𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,)𝐵)) | ||
Theorem | ioomax 12560 | The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.) |
⊢ (-∞(,)+∞) = ℝ | ||
Theorem | iccmax 12561 | The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.) |
⊢ (-∞[,]+∞) = ℝ* | ||
Theorem | ioopos 12562 | The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.) |
⊢ (0(,)+∞) = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | ||
Theorem | ioorp 12563 | The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (0(,)+∞) = ℝ+ | ||
Theorem | iooshf 12564 | Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐵) ∈ (𝐶(,)𝐷) ↔ 𝐴 ∈ ((𝐶 + 𝐵)(,)(𝐷 + 𝐵)))) | ||
Theorem | iocssre 12565 | A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ) | ||
Theorem | icossre 12566 | A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ⊆ ℝ) | ||
Theorem | iccssre 12567 | A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) | ||
Theorem | iccssxr 12568 | A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.) |
⊢ (𝐴[,]𝐵) ⊆ ℝ* | ||
Theorem | iocssxr 12569 | An open-below, closed-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.) |
⊢ (𝐴(,]𝐵) ⊆ ℝ* | ||
Theorem | icossxr 12570 | A closed-below, open-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.) |
⊢ (𝐴[,)𝐵) ⊆ ℝ* | ||
Theorem | ioossicc 12571 | An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | eliccxr 12572 | A member of a closed interval is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝐵[,]𝐶) → 𝐴 ∈ ℝ*) | ||
Theorem | icossicc 12573 | A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.) |
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | iocssicc 12574 | A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | ioossico 12575 | An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,)𝐵) | ||
Theorem | iocssioo 12576 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶(,]𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | icossioo 12577 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | ioossioo 12578 | Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | iccsupr 12579* | A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl 11337). (Contributed by Paul Chapman, 21-Jan-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑆 ⊆ (𝐴[,]𝐵) ∧ 𝐶 ∈ 𝑆) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) | ||
Theorem | elioopnf 12580 | Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))) | ||
Theorem | elioomnf 12581 | Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝐴))) | ||
Theorem | elicopnf 12582 | Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵))) | ||
Theorem | repos 12583 | Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.) |
⊢ (𝐴 ∈ (0(,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | ||
Theorem | ioof 12584 | The set of open intervals of extended reals maps to subsets of reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ | ||
Theorem | iccf 12585 | The set of closed intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ [,]:(ℝ* × ℝ*)⟶𝒫 ℝ* | ||
Theorem | unirnioo 12586 | The union of the range of the open interval function. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.) |
⊢ ℝ = ∪ ran (,) | ||
Theorem | dfioo2 12587* | Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑤 ∈ ℝ ∣ (𝑥 < 𝑤 ∧ 𝑤 < 𝑦)}) | ||
Theorem | ioorebas 12588 | Open intervals are elements of the set of all open intervals. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (𝐴(,)𝐵) ∈ ran (,) | ||
Theorem | xrge0neqmnf 12589 | A nonnegative extended real is not equal to minus infinity. (Contributed by Thierry Arnoux, 9-Jun-2017.) (Proof shortened by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐴 ∈ (0[,]+∞) → 𝐴 ≠ -∞) | ||
Theorem | xrge0neqmnfOLD 12590 | Obsolete proof of xrge0neqmnf 12589 as of 24-Jul-2022. (Contributed by Thierry Arnoux, 9-Jun-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ (0[,]+∞) → 𝐴 ≠ -∞) | ||
Theorem | xrge0nre 12591 | An extended real which is not a real is plus infinity. (Contributed by Thierry Arnoux, 16-Oct-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ ¬ 𝐴 ∈ ℝ) → 𝐴 = +∞) | ||
Theorem | elrege0 12592 | The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) | ||
Theorem | nn0rp0 12593 | A nonnegative integer is a nonnegative real number. (Contributed by AV, 24-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0[,)+∞)) | ||
Theorem | rge0ssre 12594 | Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.) |
⊢ (0[,)+∞) ⊆ ℝ | ||
Theorem | elxrge0 12595 | Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴)) | ||
Theorem | 0e0icopnf 12596 | 0 is a member of (0[,)+∞). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ∈ (0[,)+∞) | ||
Theorem | 0e0iccpnf 12597 | 0 is a member of (0[,]+∞). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ∈ (0[,]+∞) | ||
Theorem | ge0addcl 12598 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 + 𝐵) ∈ (0[,)+∞)) | ||
Theorem | ge0mulcl 12599 | The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 · 𝐵) ∈ (0[,)+∞)) | ||
Theorem | ge0xaddcl 12600 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 +𝑒 𝐵) ∈ (0[,]+∞)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |