Home | Metamath
Proof Explorer Theorem List (p. 123 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ioon0 12201 | 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 12202 | 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 12203 | 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 12204 | 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 12205 | 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 12206 | An open interval does not contain its left endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ¬ 𝐴 ∈ (𝐴(,)𝐵) | ||
Theorem | ubioo 12207 | An open interval does not contain its right endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ ¬ 𝐵 ∈ (𝐴(,)𝐵) | ||
Theorem | iooval2 12208* | Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | iooin 12209 | 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 12210 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶)) | ||
Theorem | iooss2 12211 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶)) | ||
Theorem | iocval 12212* | Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)}) | ||
Theorem | icoval 12213* | Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)}) | ||
Theorem | iccval 12214* | Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)}) | ||
Theorem | elioo1 12215 | Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elioo2 12216 | Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | elioc1 12217 | 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 12218 | 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 12219 | Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | iccid 12220 | A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.) |
⊢ (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴}) | ||
Theorem | ico0 12221 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | ioc0 12222 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴(,]𝐵) = ∅ ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | icc0 12223 | An empty closed interval of extended reals. (Contributed by FL, 30-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) | ||
Theorem | elicod 12224 | Membership in a left closed, right open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 < 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵)) | ||
Theorem | icogelb 12225 | 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 12226 | A member of a left closed, right open interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 ∈ ℝ) | ||
Theorem | ubioc1 12227 | The upper bound belongs to an open-below, closed-above interval. See ubicc2 12289. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵)) | ||
Theorem | lbico1 12228 | The lower bound belongs to a closed-below, open-above interval. See lbicc2 12288. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵)) | ||
Theorem | iccleub 12229 | An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵) | ||
Theorem | iccgelb 12230 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) | ||
Theorem | elioo5 12231 | Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | eliooxr 12232 | A nonempty open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*)) | ||
Theorem | eliooord 12233 | 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 12234 | Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | ioossre 12235 | An open interval is a set of reals. (Contributed by NM, 31-May-2007.) |
⊢ (𝐴(,)𝐵) ⊆ ℝ | ||
Theorem | elioc2 12236 | 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 12237 | 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 12238 | Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | elicc2i 12239 | Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) | ||
Theorem | elicc4 12240 | Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | iccss 12241 | 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 12242 | Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | icossico 12243 | 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 12244 | 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 12245 | Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,)𝐵)) | ||
Theorem | iccssioo2 12246 | Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
⊢ ((𝐶 ∈ (𝐴(,)𝐵) ∧ 𝐷 ∈ (𝐴(,)𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | iccssico2 12247 | 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 12248 | The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.) |
⊢ (-∞(,)+∞) = ℝ | ||
Theorem | iccmax 12249 | The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.) |
⊢ (-∞[,]+∞) = ℝ* | ||
Theorem | ioopos 12250 | The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.) |
⊢ (0(,)+∞) = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | ||
Theorem | ioorp 12251 | The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (0(,)+∞) = ℝ+ | ||
Theorem | iooshf 12252 | Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐵) ∈ (𝐶(,)𝐷) ↔ 𝐴 ∈ ((𝐶 + 𝐵)(,)(𝐷 + 𝐵)))) | ||
Theorem | iocssre 12253 | A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ) | ||
Theorem | icossre 12254 | A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ⊆ ℝ) | ||
Theorem | iccssre 12255 | 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 12256 | A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.) |
⊢ (𝐴[,]𝐵) ⊆ ℝ* | ||
Theorem | iocssxr 12257 | 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 12258 | 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 12259 | An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | icossicc 12260 | A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.) |
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | iocssicc 12261 | A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | ioossico 12262 | An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,)𝐵) | ||
Theorem | iocssioo 12263 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶(,]𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | icossioo 12264 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | ioossioo 12265 | Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | iccsupr 12266* | A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl 10983). (Contributed by Paul Chapman, 21-Jan-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑆 ⊆ (𝐴[,]𝐵) ∧ 𝐶 ∈ 𝑆) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) | ||
Theorem | elioopnf 12267 | Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))) | ||
Theorem | elioomnf 12268 | Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝐴))) | ||
Theorem | elicopnf 12269 | Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵))) | ||
Theorem | repos 12270 | Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.) |
⊢ (𝐴 ∈ (0(,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | ||
Theorem | ioof 12271 | 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 12272 | 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 12273 | 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 12274* | 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 12275 | Open intervals are elements of the set of all open intervals. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (𝐴(,)𝐵) ∈ ran (,) | ||
Theorem | xrge0neqmnf 12276 | An extended nonnegative real cannot be minus infinity. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
⊢ (𝐴 ∈ (0[,]+∞) → 𝐴 ≠ -∞) | ||
Theorem | xrge0nre 12277 | An extended real which is not a real is plus infinity. (Contributed by Thierry Arnoux, 16-Oct-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ ¬ 𝐴 ∈ ℝ) → 𝐴 = +∞) | ||
Theorem | elrege0 12278 | 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 12279 | A nonnegative integer is a nonnegative real number. (Contributed by AV, 24-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0[,)+∞)) | ||
Theorem | rge0ssre 12280 | Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.) |
⊢ (0[,)+∞) ⊆ ℝ | ||
Theorem | elxrge0 12281 | Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴)) | ||
Theorem | 0e0icopnf 12282 | 0 is a member of (0[,)+∞) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ∈ (0[,)+∞) | ||
Theorem | 0e0iccpnf 12283 | 0 is a member of (0[,]+∞) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ∈ (0[,]+∞) | ||
Theorem | ge0addcl 12284 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 + 𝐵) ∈ (0[,)+∞)) | ||
Theorem | ge0mulcl 12285 | The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 · 𝐵) ∈ (0[,)+∞)) | ||
Theorem | ge0xaddcl 12286 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 +𝑒 𝐵) ∈ (0[,]+∞)) | ||
Theorem | ge0xmulcl 12287 | The nonnegative extended reals are closed under multiplication. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 ·e 𝐵) ∈ (0[,]+∞)) | ||
Theorem | lbicc2 12288 | The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) (Revised by Mario Carneiro, 9-Sep-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) | ||
Theorem | ubicc2 12289 | The upper bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) | ||
Theorem | 0elunit 12290 | Zero is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.) |
⊢ 0 ∈ (0[,]1) | ||
Theorem | 1elunit 12291 | One is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.) |
⊢ 1 ∈ (0[,]1) | ||
Theorem | iooneg 12292 | Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴(,)𝐵) ↔ -𝐶 ∈ (-𝐵(,)-𝐴))) | ||
Theorem | iccneg 12293 | Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ -𝐶 ∈ (-𝐵[,]-𝐴))) | ||
Theorem | icoshft 12294 | A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ (𝐴[,)𝐵) → (𝑋 + 𝐶) ∈ ((𝐴 + 𝐶)[,)(𝐵 + 𝐶)))) | ||
Theorem | icoshftf1o 12295* | Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ (𝐴[,)𝐵) ↦ (𝑥 + 𝐶)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐹:(𝐴[,)𝐵)–1-1-onto→((𝐴 + 𝐶)[,)(𝐵 + 𝐶))) | ||
Theorem | icoun 12296 | The union of end-to-end closed-below, open-above real intervals. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,)𝐵) ∪ (𝐵[,)𝐶)) = (𝐴[,)𝐶)) | ||
Theorem | icodisj 12297 | End-to-end closed-below, open-above real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴[,)𝐵) ∩ (𝐵[,)𝐶)) = ∅) | ||
Theorem | snunioo 12298 | The closure of one end of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵)) | ||
Theorem | snunico 12299 | The closure of the open end of a right-open real interval. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴[,)𝐵) ∪ {𝐵}) = (𝐴[,]𝐵)) | ||
Theorem | snunioc 12300 | The closure of the open end of a left-open real interval. (Contributed by Thierry Arnoux, 28-Mar-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ({𝐴} ∪ (𝐴(,]𝐵)) = (𝐴[,]𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |