![]() |
Metamath
Proof Explorer Theorem List (p. 134 of 472) | < 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-29689) |
![]() (29690-31212) |
![]() (31213-47147) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iccssre 13301 | 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 13302 | A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.) |
⊢ (𝐴[,]𝐵) ⊆ ℝ* | ||
Theorem | iocssxr 13303 | 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 13304 | 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 13305 | An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | iccssred 13306 | A closed real interval is a set of reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) | ||
Theorem | eliccxr 13307 | A member of a closed interval is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝐵[,]𝐶) → 𝐴 ∈ ℝ*) | ||
Theorem | icossicc 13308 | A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.) |
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | iocssicc 13309 | A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵) | ||
Theorem | ioossico 13310 | An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,)𝐵) | ||
Theorem | iocssioo 13311 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶(,]𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | icossioo 13312 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | ioossioo 13313 | Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵)) | ||
Theorem | iccsupr 13314* | A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl 12074). (Contributed by Paul Chapman, 21-Jan-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑆 ⊆ (𝐴[,]𝐵) ∧ 𝐶 ∈ 𝑆) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) | ||
Theorem | elioopnf 13315 | Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))) | ||
Theorem | elioomnf 13316 | Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝐴))) | ||
Theorem | elicopnf 13317 | Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵))) | ||
Theorem | repos 13318 | Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.) |
⊢ (𝐴 ∈ (0(,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | ||
Theorem | ioof 13319 | 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 13320 | 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 13321 | 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 13322* | 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 13323 | Open intervals are elements of the set of all open intervals. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (𝐴(,)𝐵) ∈ ran (,) | ||
Theorem | xrge0neqmnf 13324 | 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 | xrge0nre 13325 | An extended real which is not a real is plus infinity. (Contributed by Thierry Arnoux, 16-Oct-2017.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ ¬ 𝐴 ∈ ℝ) → 𝐴 = +∞) | ||
Theorem | elrege0 13326 | 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 13327 | A nonnegative integer is a nonnegative real number. (Contributed by AV, 24-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0[,)+∞)) | ||
Theorem | rge0ssre 13328 | Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.) |
⊢ (0[,)+∞) ⊆ ℝ | ||
Theorem | elxrge0 13329 | Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴)) | ||
Theorem | 0e0icopnf 13330 | 0 is a member of (0[,)+∞). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ∈ (0[,)+∞) | ||
Theorem | 0e0iccpnf 13331 | 0 is a member of (0[,]+∞). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ∈ (0[,]+∞) | ||
Theorem | ge0addcl 13332 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 + 𝐵) ∈ (0[,)+∞)) | ||
Theorem | ge0mulcl 13333 | The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 · 𝐵) ∈ (0[,)+∞)) | ||
Theorem | ge0xaddcl 13334 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 +𝑒 𝐵) ∈ (0[,]+∞)) | ||
Theorem | ge0xmulcl 13335 | The nonnegative extended reals are closed under multiplication. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 ·e 𝐵) ∈ (0[,]+∞)) | ||
Theorem | lbicc2 13336 | 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 13337 | 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 | elicc01 13338 | Membership in the closed real interval between 0 and 1, also called the closed unit interval. (Contributed by AV, 20-Aug-2022.) |
⊢ (𝑋 ∈ (0[,]1) ↔ (𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1)) | ||
Theorem | elunitrn 13339 | The closed unit interval is a subset of the set of the real numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 21-Dec-2016.) |
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈ ℝ) | ||
Theorem | elunitcn 13340 | The closed unit interval is a subset of the set of the complex numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 21-Dec-2016.) |
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈ ℂ) | ||
Theorem | 0elunit 13341 | Zero is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.) |
⊢ 0 ∈ (0[,]1) | ||
Theorem | 1elunit 13342 | One is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.) |
⊢ 1 ∈ (0[,]1) | ||
Theorem | iooneg 13343 | Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴(,)𝐵) ↔ -𝐶 ∈ (-𝐵(,)-𝐴))) | ||
Theorem | iccneg 13344 | Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ -𝐶 ∈ (-𝐵[,]-𝐴))) | ||
Theorem | icoshft 13345 | A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ (𝐴[,)𝐵) → (𝑋 + 𝐶) ∈ ((𝐴 + 𝐶)[,)(𝐵 + 𝐶)))) | ||
Theorem | icoshftf1o 13346* | 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 13347 | The union of two adjacent left-closed right-open real intervals is a left-closed right-open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,)𝐵) ∪ (𝐵[,)𝐶)) = (𝐴[,)𝐶)) | ||
Theorem | icodisj 13348 | Adjacent left-closed right-open real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴[,)𝐵) ∩ (𝐵[,)𝐶)) = ∅) | ||
Theorem | ioounsn 13349 | The union of an open interval with its upper endpoint is a left-open right-closed interval. (Contributed by Jon Pennant, 8-Jun-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵)) | ||
Theorem | snunioo 13350 | 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 13351 | The closure of the open end of a right-open real interval. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴[,)𝐵) ∪ {𝐵}) = (𝐴[,]𝐵)) | ||
Theorem | snunioc 13352 | The closure of the open end of a left-open real interval. (Contributed by Thierry Arnoux, 28-Mar-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ({𝐴} ∪ (𝐴(,]𝐵)) = (𝐴[,]𝐵)) | ||
Theorem | prunioo 13353 | The closure of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) | ||
Theorem | ioodisj 13354 | 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 13355 | Join two open intervals to create a third. (Contributed by NM, 11-Aug-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (((𝐴(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)𝐶)) = (𝐴(,)𝐶)) | ||
Theorem | difreicc 13356 | The class difference of ℝ and a closed interval. (Contributed by FL, 18-Jun-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (ℝ ∖ (𝐴[,]𝐵)) = ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) | ||
Theorem | iccsplit 13357 | Split a closed interval into the union of two closed intervals. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = ((𝐴[,]𝐶) ∪ (𝐶[,]𝐵))) | ||
Theorem | iccshftr 13358 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 + 𝑅) = 𝐶 & ⊢ (𝐵 + 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 + 𝑅) ∈ (𝐶[,]𝐷))) | ||
Theorem | iccshftri 13359 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ & ⊢ (𝐴 + 𝑅) = 𝐶 & ⊢ (𝐵 + 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 + 𝑅) ∈ (𝐶[,]𝐷)) | ||
Theorem | iccshftl 13360 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 − 𝑅) = 𝐶 & ⊢ (𝐵 − 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 − 𝑅) ∈ (𝐶[,]𝐷))) | ||
Theorem | iccshftli 13361 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ & ⊢ (𝐴 − 𝑅) = 𝐶 & ⊢ (𝐵 − 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 − 𝑅) ∈ (𝐶[,]𝐷)) | ||
Theorem | iccdil 13362 | Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 · 𝑅) = 𝐶 & ⊢ (𝐵 · 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 · 𝑅) ∈ (𝐶[,]𝐷))) | ||
Theorem | iccdili 13363 | Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ+ & ⊢ (𝐴 · 𝑅) = 𝐶 & ⊢ (𝐵 · 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 · 𝑅) ∈ (𝐶[,]𝐷)) | ||
Theorem | icccntr 13364 | Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 / 𝑅) = 𝐶 & ⊢ (𝐵 / 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 / 𝑅) ∈ (𝐶[,]𝐷))) | ||
Theorem | icccntri 13365 | Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ+ & ⊢ (𝐴 / 𝑅) = 𝐶 & ⊢ (𝐵 / 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 / 𝑅) ∈ (𝐶[,]𝐷)) | ||
Theorem | divelunit 13366 | A condition for a ratio to be a member of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐴 / 𝐵) ∈ (0[,]1) ↔ 𝐴 ≤ 𝐵)) | ||
Theorem | lincmb01cmp 13367 | 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 13368* | 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 13369 | 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 13370 | 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 13371 | (0[,]1) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (0[,]1) ⊆ ℝ | ||
Theorem | unitsscn 13372 | The closed unit interval is a subset of the set of the complex numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
⊢ (0[,]1) ⊆ ℂ | ||
Theorem | supicc 13373 | Supremum of a bounded set of real numbers. (Contributed by Thierry Arnoux, 17-May-2019.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶)) | ||
Theorem | supiccub 13374 | The supremum of a bounded set of real numbers is an upper bound. (Contributed by Thierry Arnoux, 20-May-2019.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐷 ≤ sup(𝐴, ℝ, < )) | ||
Theorem | supicclub 13375* | The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐷 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐷 < 𝑧)) | ||
Theorem | supicclub2 13376* | The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ≤ 𝐷) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐷) | ||
Theorem | zltaddlt1le 13377 | 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 13378 | An extended nonnegative integer is an extended nonnegative real. (Contributed by AV, 10-Dec-2020.) |
⊢ (𝐴 ∈ ℕ0* → 𝐴 ∈ (0[,]+∞)) | ||
Syntax | cfz 13379 |
Extend class notation to include the notation for a contiguous finite set
of integers. Read "𝑀...𝑁 " as "the set of integers
from 𝑀 to
𝑁 inclusive".
This symbol is also used informally in some comments to denote an ellipsis, e.g., 𝐴 + 𝐴↑2 + ... + 𝐴↑(𝑁 − 1). |
class ... | ||
Definition | df-fz 13380* | Define an operation that produces a finite set of sequential integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive". See fzval 13381 for its value and additional comments. (Contributed by NM, 6-Sep-2005.) |
⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)}) | ||
Theorem | fzval 13381* | 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 13382 | An alternative way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) | ||
Theorem | fzf 13383 | Establish the domain and codomain of the finite integer sequence function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 16-Nov-2013.) |
⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ | ||
Theorem | elfz1 13384 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfz 13385 | Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfz2 13386 | Membership in a finite set of sequential integers. We use the fact that an operation's value is empty outside of its domain to show 𝑀 ∈ ℤ and 𝑁 ∈ ℤ. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfzd 13387 | Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝐾) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) | ||
Theorem | elfz5 13388 | Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.) |
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾 ≤ 𝑁)) | ||
Theorem | elfz4 13389 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝐾 ∈ (𝑀...𝑁)) | ||
Theorem | elfzuzb 13390 | Membership in a finite set of sequential integers in terms of sets of upper integers. (Contributed by NM, 18-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾))) | ||
Theorem | eluzfz 13391 | Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁)) | ||
Theorem | elfzuz 13392 | A member of a finite set of sequential integers belongs to an upper set of integers. (Contributed by NM, 17-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) | ||
Theorem | elfzuz3 13393 | Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) | ||
Theorem | elfzel2 13394 | Membership in a finite set of sequential integer implies the upper bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ) | ||
Theorem | elfzel1 13395 | Membership in a finite set of sequential integer implies the lower bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ) | ||
Theorem | elfzelz 13396 | A member of a finite set of sequential integers is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ) | ||
Theorem | elfzelzd 13397 | A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → 𝐾 ∈ ℤ) | ||
Theorem | fzssz 13398 | A finite sequence of integers is a set of integers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝑀...𝑁) ⊆ ℤ | ||
Theorem | elfzle1 13399 | A member of a finite set of sequential integer is greater than or equal to the lower bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾) | ||
Theorem | elfzle2 13400 | A member of a finite set of sequential integer is less than or equal to the upper bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |