| Metamath
Proof Explorer Theorem List (p. 136 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ge0mulcl 13501 | The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.) |
| ⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 · 𝐵) ∈ (0[,)+∞)) | ||
| Theorem | ge0xaddcl 13502 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 +𝑒 𝐵) ∈ (0[,]+∞)) | ||
| Theorem | ge0xmulcl 13503 | The nonnegative extended reals are closed under multiplication. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 ·e 𝐵) ∈ (0[,]+∞)) | ||
| Theorem | lbicc2 13504 | 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 13505 | 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 13506 | 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 13507 | 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 13508 | 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 13509 | Zero is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.) |
| ⊢ 0 ∈ (0[,]1) | ||
| Theorem | 1elunit 13510 | One is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.) |
| ⊢ 1 ∈ (0[,]1) | ||
| Theorem | iooneg 13511 | Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴(,)𝐵) ↔ -𝐶 ∈ (-𝐵(,)-𝐴))) | ||
| Theorem | iccneg 13512 | Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ -𝐶 ∈ (-𝐵[,]-𝐴))) | ||
| Theorem | icoshft 13513 | A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ (𝐴[,)𝐵) → (𝑋 + 𝐶) ∈ ((𝐴 + 𝐶)[,)(𝐵 + 𝐶)))) | ||
| Theorem | icoshftf1o 13514* | 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 13515 | 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 13516 | Adjacent left-closed right-open real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴[,)𝐵) ∩ (𝐵[,)𝐶)) = ∅) | ||
| Theorem | ioounsn 13517 | 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 13518 | 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 13519 | The closure of the open end of a right-open real interval. (Contributed by Mario Carneiro, 16-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴[,)𝐵) ∪ {𝐵}) = (𝐴[,]𝐵)) | ||
| Theorem | snunioc 13520 | The closure of the open end of a left-open real interval. (Contributed by Thierry Arnoux, 28-Mar-2017.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ({𝐴} ∪ (𝐴(,]𝐵)) = (𝐴[,]𝐵)) | ||
| Theorem | prunioo 13521 | The closure of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) | ||
| Theorem | ioodisj 13522 | 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 13523 | Join two open intervals to create a third. (Contributed by NM, 11-Aug-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (((𝐴(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)𝐶)) = (𝐴(,)𝐶)) | ||
| Theorem | difreicc 13524 | The class difference of ℝ and a closed interval. (Contributed by FL, 18-Jun-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (ℝ ∖ (𝐴[,]𝐵)) = ((-∞(,)𝐴) ∪ (𝐵(,)+∞))) | ||
| Theorem | iccsplit 13525 | Split a closed interval into the union of two closed intervals. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = ((𝐴[,]𝐶) ∪ (𝐶[,]𝐵))) | ||
| Theorem | iccshftr 13526 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐴 + 𝑅) = 𝐶 & ⊢ (𝐵 + 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 + 𝑅) ∈ (𝐶[,]𝐷))) | ||
| Theorem | iccshftri 13527 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ & ⊢ (𝐴 + 𝑅) = 𝐶 & ⊢ (𝐵 + 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 + 𝑅) ∈ (𝐶[,]𝐷)) | ||
| Theorem | iccshftl 13528 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐴 − 𝑅) = 𝐶 & ⊢ (𝐵 − 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 − 𝑅) ∈ (𝐶[,]𝐷))) | ||
| Theorem | iccshftli 13529 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ & ⊢ (𝐴 − 𝑅) = 𝐶 & ⊢ (𝐵 − 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 − 𝑅) ∈ (𝐶[,]𝐷)) | ||
| Theorem | iccdil 13530 | Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐴 · 𝑅) = 𝐶 & ⊢ (𝐵 · 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 · 𝑅) ∈ (𝐶[,]𝐷))) | ||
| Theorem | iccdili 13531 | Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ+ & ⊢ (𝐴 · 𝑅) = 𝐶 & ⊢ (𝐵 · 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 · 𝑅) ∈ (𝐶[,]𝐷)) | ||
| Theorem | icccntr 13532 | Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝐴 / 𝑅) = 𝐶 & ⊢ (𝐵 / 𝑅) = 𝐷 ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 / 𝑅) ∈ (𝐶[,]𝐷))) | ||
| Theorem | icccntri 13533 | Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝑅 ∈ ℝ+ & ⊢ (𝐴 / 𝑅) = 𝐶 & ⊢ (𝐵 / 𝑅) = 𝐷 ⇒ ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 / 𝑅) ∈ (𝐶[,]𝐷)) | ||
| Theorem | divelunit 13534 | 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 13535 | 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 13536* | 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 13537 | 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 13538 | 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 13539 | (0[,]1) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (0[,]1) ⊆ ℝ | ||
| Theorem | unitsscn 13540 | 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 13541 | Supremum of a bounded set of real numbers. (Contributed by Thierry Arnoux, 17-May-2019.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶)) | ||
| Theorem | supiccub 13542 | The supremum of a bounded set of real numbers is an upper bound. (Contributed by Thierry Arnoux, 20-May-2019.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐷 ≤ sup(𝐴, ℝ, < )) | ||
| Theorem | supicclub 13543* | The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐷 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐷 < 𝑧)) | ||
| Theorem | supicclub2 13544* | The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ≤ 𝐷) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐷) | ||
| Theorem | zltaddlt1le 13545 | 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 13546 | An extended nonnegative integer is an extended nonnegative real. (Contributed by AV, 10-Dec-2020.) |
| ⊢ (𝐴 ∈ ℕ0* → 𝐴 ∈ (0[,]+∞)) | ||
| Syntax | cfz 13547 |
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 13548* | Define an operation that produces a finite set of sequential integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive". See fzval 13549 for its value and additional comments. (Contributed by NM, 6-Sep-2005.) |
| ⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)}) | ||
| Theorem | fzval 13549* | 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 13550 | An alternative way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) | ||
| Theorem | fzf 13551 | 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 13552 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | ||
| Theorem | elfz 13553 | Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | ||
| Theorem | elfz2 13554 | 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 13555 | Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝐾) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) | ||
| Theorem | elfz5 13556 | Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.) |
| ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾 ≤ 𝑁)) | ||
| Theorem | elfz4 13557 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝐾 ∈ (𝑀...𝑁)) | ||
| Theorem | elfzuzb 13558 | 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 13559 | Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁)) | ||
| Theorem | elfzuz 13560 | 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 13561 | 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 13562 | 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 13563 | 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 13564 | 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 13565 | A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → 𝐾 ∈ ℤ) | ||
| Theorem | fzssz 13566 | A finite sequence of integers is a set of integers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝑀...𝑁) ⊆ ℤ | ||
| Theorem | elfzle1 13567 | 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 13568 | 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.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁) | ||
| Theorem | elfzuz2 13569 | Implication of membership in a finite set of sequential integers. (Contributed by NM, 20-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) | ||
| Theorem | elfzle3 13570 | Membership in a finite set of sequential integer implies the bounds are comparable. (Contributed by NM, 18-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑁) | ||
| Theorem | eluzfz1 13571 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) | ||
| Theorem | eluzfz2 13572 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 13-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) | ||
| Theorem | eluzfz2b 13573 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑁 ∈ (𝑀...𝑁)) | ||
| Theorem | elfz3 13574 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.) |
| ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (𝑁...𝑁)) | ||
| Theorem | elfz1eq 13575 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.) |
| ⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁) | ||
| Theorem | elfzubelfz 13576 | If there is a member in a finite set of sequential integers, the upper bound is also a member of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 31-May-2018.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (𝑀...𝑁)) | ||
| Theorem | peano2fzr 13577 | A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.) |
| ⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ (𝐾 + 1) ∈ (𝑀...𝑁)) → 𝐾 ∈ (𝑀...𝑁)) | ||
| Theorem | fzn0 13578 | Properties of a finite interval of integers which is nonempty. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀)) | ||
| Theorem | fz0 13579 | A finite set of sequential integers is empty if its bounds are not integers. (Contributed by AV, 13-Oct-2018.) |
| ⊢ ((𝑀 ∉ ℤ ∨ 𝑁 ∉ ℤ) → (𝑀...𝑁) = ∅) | ||
| Theorem | fzn 13580 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅)) | ||
| Theorem | fzen 13581 | A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) | ||
| Theorem | fz1n 13582 | A 1-based finite set of sequential integers is empty iff it ends at index 0. (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ (𝑁 ∈ ℕ0 → ((1...𝑁) = ∅ ↔ 𝑁 = 0)) | ||
| Theorem | 0nelfz1 13583 | 0 is not an element of a finite interval of integers starting at 1. (Contributed by AV, 27-Aug-2020.) |
| ⊢ 0 ∉ (1...𝑁) | ||
| Theorem | 0fz1 13584 | Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (1...𝑁)) → (𝐹 = ∅ ↔ 𝑁 = 0)) | ||
| Theorem | fz10 13585 | There are no integers between 1 and 0. (Contributed by Jeff Madsen, 16-Jun-2010.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (1...0) = ∅ | ||
| Theorem | uzsubsubfz 13586 | Membership of an integer greater than L decreased by ( L - M ) in an M-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.) |
| ⊢ ((𝐿 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐿)) → (𝑁 − (𝐿 − 𝑀)) ∈ (𝑀...𝑁)) | ||
| Theorem | uzsubsubfz1 13587 | Membership of an integer greater than L decreased by ( L - 1 ) in a 1-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.) |
| ⊢ ((𝐿 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝐿)) → (𝑁 − (𝐿 − 1)) ∈ (1...𝑁)) | ||
| Theorem | ige3m2fz 13588 | Membership of an integer greater than 2 decreased by 2 in a 1-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.) |
| ⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑁 − 2) ∈ (1...𝑁)) | ||
| Theorem | fzsplit2 13589 | Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
| ⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁))) | ||
| Theorem | fzsplit 13590 | Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 13-Apr-2016.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁))) | ||
| Theorem | fzdisj 13591 | Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.) |
| ⊢ (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅) | ||
| Theorem | fz01en 13592 | 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.) |
| ⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁)) | ||
| Theorem | elfznn 13593 | A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005.) |
| ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ) | ||
| Theorem | elfz1end 13594 | A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
| ⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴)) | ||
| Theorem | fz1ssnn 13595 | A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
| ⊢ (1...𝐴) ⊆ ℕ | ||
| Theorem | fznn0sub 13596 | Subtraction closure for a member of a finite set of sequential integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑁 − 𝐾) ∈ ℕ0) | ||
| Theorem | fzmmmeqm 13597 | Subtracting the difference of a member of a finite range of integers and the lower bound of the range from the difference of the upper bound and the lower bound of the range results in the difference of the upper bound of the range and the member. (Contributed by Alexander van der Vekens, 27-May-2018.) |
| ⊢ (𝑀 ∈ (𝐿...𝑁) → ((𝑁 − 𝐿) − (𝑀 − 𝐿)) = (𝑁 − 𝑀)) | ||
| Theorem | fzaddel 13598 | Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
| ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) | ||
| Theorem | fzadd2 13599 | Membership of a sum in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
| ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ)) → ((𝐽 ∈ (𝑀...𝑁) ∧ 𝐾 ∈ (𝑂...𝑃)) → (𝐽 + 𝐾) ∈ ((𝑀 + 𝑂)...(𝑁 + 𝑃)))) | ||
| Theorem | fzsubel 13600 | Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
| ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾)))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |