Home | Metamath
Proof Explorer Theorem List (p. 122 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 | iccgelb 12101 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) | ||
Theorem | elioo5 12102 | Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | eliooxr 12103 | A nonempty open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*)) | ||
Theorem | eliooord 12104 | 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 12105 | Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | ||
Theorem | ioossre 12106 | An open interval is a set of reals. (Contributed by NM, 31-May-2007.) |
⊢ (𝐴(,)𝐵) ⊆ ℝ | ||
Theorem | elioc2 12107 | 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 12108 | 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 12109 | Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | elicc2i 12110 | Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) | ||
Theorem | elicc4 12111 | Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | ||
Theorem | iccss 12112 | 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 12113 | Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | icossico 12114 | 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 12115 | 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 12116 | Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,)𝐵)) | ||
Theorem | iccssioo2 12117 | Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
⊢ ((𝐶 ∈ (𝐴(,)𝐵) ∧ 𝐷 ∈ (𝐴(,)𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | iccssico2 12118 | 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 12119 | The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.) |
⊢ (-∞(,)+∞) = ℝ | ||
Theorem | iccmax 12120 | The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.) |
⊢ (-∞[,]+∞) = ℝ* | ||
Theorem | ioopos 12121 | The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.) |
⊢ (0(,)+∞) = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | ||
Theorem | ioorp 12122 | The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ (0(,)+∞) = ℝ+ | ||
Theorem | iooshf 12123 | Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐵) ∈ (𝐶(,)𝐷) ↔ 𝐴 ∈ ((𝐶 + 𝐵)(,)(𝐷 + 𝐵)))) | ||
Theorem | iocssre 12124 | A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ) | ||
Theorem | icossre 12125 | A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ⊆ ℝ) | ||
Theorem | iccssre 12126 | 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 12127 | A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.) |
⊢ (𝐴[,]𝐵) ⊆ ℝ* | ||
Theorem | iocssxr 12128 | 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 12129 | 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 12130 | An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | icossicc 12131 | A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.) |
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | iocssicc 12132 | A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | ioossico 12133 | An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,)𝐵) | ||
Theorem | iocssioo 12134 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶(,]𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | icossioo 12135 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | ioossioo 12136 | Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | iccsupr 12137* | A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl 10862). (Contributed by Paul Chapman, 21-Jan-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑆 ⊆ (𝐴[,]𝐵) ∧ 𝐶 ∈ 𝑆) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) | ||
Theorem | elioopnf 12138 | Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))) | ||
Theorem | elioomnf 12139 | Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝐴))) | ||
Theorem | elicopnf 12140 | Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵))) | ||
Theorem | repos 12141 | Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.) |
⊢ (𝐴 ∈ (0(,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | ||
Theorem | ioof 12142 | 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 12143 | 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 12144 | 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 12145* | 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 12146 | Open intervals are elements of the set of all open intervals. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (𝐴(,)𝐵) ∈ ran (,) | ||
Theorem | xrge0neqmnf 12147 | An extended nonnegative real cannot be minus infinity. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
⊢ (𝐴 ∈ (0[,]+∞) → 𝐴 ≠ -∞) | ||
Theorem | xrge0nre 12148 | An extended real which is not a real is plus infinity. (Contributed by Thierry Arnoux, 16-Oct-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ ¬ 𝐴 ∈ ℝ) → 𝐴 = +∞) | ||
Theorem | elrege0 12149 | 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 12150 | A nonnegative integer is a nonnegative real number. (Contributed by AV, 24-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0[,)+∞)) | ||
Theorem | rge0ssre 12151 | Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.) |
⊢ (0[,)+∞) ⊆ ℝ | ||
Theorem | elxrge0 12152 | Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴)) | ||
Theorem | 0e0icopnf 12153 | 0 is a member of (0[,)+∞) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ∈ (0[,)+∞) | ||
Theorem | 0e0iccpnf 12154 | 0 is a member of (0[,]+∞) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ∈ (0[,]+∞) | ||
Theorem | ge0addcl 12155 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 + 𝐵) ∈ (0[,)+∞)) | ||
Theorem | ge0mulcl 12156 | The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 · 𝐵) ∈ (0[,)+∞)) | ||
Theorem | ge0xaddcl 12157 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 +𝑒 𝐵) ∈ (0[,]+∞)) | ||
Theorem | ge0xmulcl 12158 | The nonnegative extended reals are closed under multiplication. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 ·e 𝐵) ∈ (0[,]+∞)) | ||
Theorem | lbicc2 12159 | 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 12160 | 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 12161 | Zero is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.) |
⊢ 0 ∈ (0[,]1) | ||
Theorem | 1elunit 12162 | One is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.) |
⊢ 1 ∈ (0[,]1) | ||
Theorem | iooneg 12163 | Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴(,)𝐵) ↔ -𝐶 ∈ (-𝐵(,)-𝐴))) | ||
Theorem | iccneg 12164 | Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ -𝐶 ∈ (-𝐵[,]-𝐴))) | ||
Theorem | icoshft 12165 | A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ (𝐴[,)𝐵) → (𝑋 + 𝐶) ∈ ((𝐴 + 𝐶)[,)(𝐵 + 𝐶)))) | ||
Theorem | icoshftf1o 12166* | 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 12167 | 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 12168 | End-to-end closed-below, open-above real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴[,)𝐵) ∩ (𝐵[,)𝐶)) = ∅) | ||
Theorem | snunioo 12169 | 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 12170 | The closure of the open end of a right-open real interval. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴[,)𝐵) ∪ {𝐵}) = (𝐴[,]𝐵)) | ||
Theorem | snunioc 12171 | The closure of the open end of a left-open real interval. (Contributed by Thierry Arnoux, 28-Mar-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ({𝐴} ∪ (𝐴(,]𝐵)) = (𝐴[,]𝐵)) | ||
Theorem | prunioo 12172 | The closure of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) | ||
Theorem | ioodisj 12173 | If the upper bound of one open interval is less than or equal to the lower bound of the other, the intervals are disjoint. (Contributed by Jeff Hankins, 13-Jul-2009.) |
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) ∧ 𝐵 ≤ 𝐶) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = ∅) | ||
Theorem | ioojoin 12174 | Join two open intervals to create a third. (Contributed by NM, 11-Aug-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (((𝐴(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)𝐶)) = (𝐴(,)𝐶)) | ||
Theorem | difreicc 12175 | The class difference of ℝ and a closed interval. (Contributed by FL, 18-Jun-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (ℝ ∖ (𝐴[,]𝐵)) = ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) | ||
Theorem | iccsplit 12176 | Split a closed interval into the union of two closed intervals. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = ((𝐴[,]𝐶) ∪ (𝐶[,]𝐵))) | ||
Theorem | iccshftr 12177 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 + 𝑅) = 𝐶 & ⊢ (𝐵 + 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 + 𝑅) ∈ (𝐶[,]𝐷))) | ||
Theorem | iccshftri 12178 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ & ⊢ (𝐴 + 𝑅) = 𝐶 & ⊢ (𝐵 + 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 + 𝑅) ∈ (𝐶[,]𝐷)) | ||
Theorem | iccshftl 12179 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 − 𝑅) = 𝐶 & ⊢ (𝐵 − 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 − 𝑅) ∈ (𝐶[,]𝐷))) | ||
Theorem | iccshftli 12180 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ & ⊢ (𝐴 − 𝑅) = 𝐶 & ⊢ (𝐵 − 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 − 𝑅) ∈ (𝐶[,]𝐷)) | ||
Theorem | iccdil 12181 | Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 · 𝑅) = 𝐶 & ⊢ (𝐵 · 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 · 𝑅) ∈ (𝐶[,]𝐷))) | ||
Theorem | iccdili 12182 | Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ+ & ⊢ (𝐴 · 𝑅) = 𝐶 & ⊢ (𝐵 · 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 · 𝑅) ∈ (𝐶[,]𝐷)) | ||
Theorem | icccntr 12183 | Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 / 𝑅) = 𝐶 & ⊢ (𝐵 / 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 / 𝑅) ∈ (𝐶[,]𝐷))) | ||
Theorem | icccntri 12184 | Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ+ & ⊢ (𝐴 / 𝑅) = 𝐶 & ⊢ (𝐵 / 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 / 𝑅) ∈ (𝐶[,]𝐷)) | ||
Theorem | divelunit 12185 | A condition for a ratio to be a member of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐴 / 𝐵) ∈ (0[,]1) ↔ 𝐴 ≤ 𝐵)) | ||
Theorem | lincmb01cmp 12186 | A linear combination of two reals which lies in the interval between them. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 8-Sep-2015.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) ∈ (𝐴[,]𝐵)) | ||
Theorem | iccf1o 12187* | Describe a bijection from [0, 1] to an arbitrary nontrivial closed interval [𝐴, 𝐵]. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) ∧ ◡𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴))))) | ||
Theorem | iccen 12188 | Any nontrivial closed interval is equinumerous to the unit interval. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 8-Sep-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (0[,]1) ≈ (𝐴[,]𝐵)) | ||
Theorem | xov1plusxeqvd 12189 | A complex number 𝑋 is positive real iff 𝑋 / (1 + 𝑋) is in (0(,)1). Deduction form. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ -1) ⇒ ⊢ (𝜑 → (𝑋 ∈ ℝ+ ↔ (𝑋 / (1 + 𝑋)) ∈ (0(,)1))) | ||
Theorem | unitssre 12190 | (0[,]1) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (0[,]1) ⊆ ℝ | ||
Theorem | supicc 12191 | Supremum of a bounded set of real numbers. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶)) | ||
Theorem | supiccub 12192 | The supremum of a bounded set of real numbers is an upper bound. (Contributed by Thierry Arnoux, 20-May-2019.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐷 ≤ sup(𝐴, ℝ, < )) | ||
Theorem | supicclub 12193* | The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐷 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐷 < 𝑧)) | ||
Theorem | supicclub2 12194* | The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ≤ 𝐷) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐷) | ||
Theorem | zltaddlt1le 12195 | The sum of an integer and a real number between 0 and 1 is less than or equal to a second integer iff the sum is less than the second integer. (Contributed by AV, 1-Jul-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ (0(,)1)) → ((𝑀 + 𝐴) < 𝑁 ↔ (𝑀 + 𝐴) ≤ 𝑁)) | ||
Theorem | xnn0xrge0 12196 | An extended nonnegative integer is an extended nonnegative real. (Contributed by AV, 10-Dec-2020.) |
⊢ (𝐴 ∈ ℕ0* → 𝐴 ∈ (0[,]+∞)) | ||
Syntax | cfz 12197 | Extend class notation to include the notation for a contiguous finite set of integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive." |
class ... | ||
Definition | df-fz 12198* | Define an operation that produces a finite set of sequential integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive." See fzval 12199 for its value and additional comments. (Contributed by NM, 6-Sep-2005.) |
⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)}) | ||
Theorem | fzval 12199* | The value of a finite set of sequential integers. E.g., 2...5 means the set {2, 3, 4, 5}. A special case of this definition (starting at 1) appears as Definition 11-2.1 of [Gleason] p. 141, where ℕ_k means our 1...𝑘; he calls these sets segments of the integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = {𝑘 ∈ ℤ ∣ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)}) | ||
Theorem | fzval2 12200 | An alternative way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |