| Metamath
Proof Explorer Theorem List (p. 137 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 | fzopth 13601 | A finite set of sequential integers has the ordered pair property (compare opth 5481) under certain conditions. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾))) | ||
| Theorem | fzass4 13602 | Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ ((𝐵 ∈ (𝐴...𝐷) ∧ 𝐶 ∈ (𝐵...𝐷)) ↔ (𝐵 ∈ (𝐴...𝐶) ∧ 𝐶 ∈ (𝐴...𝐷))) | ||
| Theorem | fzss1 13603 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) | ||
| Theorem | fzss2 13604 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁)) | ||
| Theorem | fzssuz 13605 | A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
| ⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀) | ||
| Theorem | fzsn 13606 | A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) | ||
| Theorem | fzssp1 13607 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1)) | ||
| Theorem | fzssnn 13608 | Finite sets of sequential integers starting from a natural are a subset of the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
| ⊢ (𝑀 ∈ ℕ → (𝑀...𝑁) ⊆ ℕ) | ||
| Theorem | ssfzunsnext 13609 | A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 13-Nov-2021.) |
| ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑆 ∪ {𝐼}) ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) | ||
| Theorem | ssfzunsn 13610 | A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 8-Jun-2021.) (Proof shortened by AV, 13-Nov-2021.) |
| ⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝑆 ∪ {𝐼}) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) | ||
| Theorem | fzsuc 13611 | Join a successor to the end of a finite set of sequential integers. (Contributed by NM, 19-Jul-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)})) | ||
| Theorem | fzpred 13612 | Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) | ||
| Theorem | fzpreddisj 13613 | A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ({𝑀} ∩ ((𝑀 + 1)...𝑁)) = ∅) | ||
| Theorem | elfzp1 13614 | Append an element to a finite set of sequential integers. (Contributed by NM, 19-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1)))) | ||
| Theorem | fzp1ss 13615 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) | ||
| Theorem | fzelp1 13616 | Membership in a set of sequential integers with an appended element. (Contributed by NM, 7-Dec-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (𝑀...(𝑁 + 1))) | ||
| Theorem | fzp1elp1 13617 | Add one to an element of a finite set of integers. (Contributed by Jeff Madsen, 6-Jun-2010.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → (𝐾 + 1) ∈ (𝑀...(𝑁 + 1))) | ||
| Theorem | fznatpl1 13618 | Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁)) | ||
| Theorem | fzpr 13619 | A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)}) | ||
| Theorem | fztp 13620 | A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 7-Mar-2014.) |
| ⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 2)) = {𝑀, (𝑀 + 1), (𝑀 + 2)}) | ||
| Theorem | fz12pr 13621 | An integer range between 1 and 2 is a pair. (Contributed by AV, 11-Jan-2023.) |
| ⊢ (1...2) = {1, 2} | ||
| Theorem | fzsuc2 13622 | Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)})) | ||
| Theorem | fzp1disj 13623 | (𝑀...(𝑁 + 1)) is the disjoint union of (𝑀...𝑁) with {(𝑁 + 1)}. (Contributed by Mario Carneiro, 7-Mar-2014.) |
| ⊢ ((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅ | ||
| Theorem | fzdifsuc 13624 | Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) | ||
| Theorem | fzprval 13625* | Two ways of defining the first two values of a sequence on ℕ. (Contributed by NM, 5-Sep-2011.) |
| ⊢ (∀𝑥 ∈ (1...2)(𝐹‘𝑥) = if(𝑥 = 1, 𝐴, 𝐵) ↔ ((𝐹‘1) = 𝐴 ∧ (𝐹‘2) = 𝐵)) | ||
| Theorem | fztpval 13626* | Two ways of defining the first three values of a sequence on ℕ. (Contributed by NM, 13-Sep-2011.) |
| ⊢ (∀𝑥 ∈ (1...3)(𝐹‘𝑥) = if(𝑥 = 1, 𝐴, if(𝑥 = 2, 𝐵, 𝐶)) ↔ ((𝐹‘1) = 𝐴 ∧ (𝐹‘2) = 𝐵 ∧ (𝐹‘3) = 𝐶)) | ||
| Theorem | fzrev 13627 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
| ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)) ↔ (𝐽 − 𝐾) ∈ (𝑀...𝑁))) | ||
| Theorem | fzrev2 13628 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
| ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)))) | ||
| Theorem | fzrev2i 13629 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
| ⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀))) | ||
| Theorem | fzrev3 13630 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
| ⊢ (𝐾 ∈ ℤ → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁))) | ||
| Theorem | fzrev3i 13631 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁)) | ||
| Theorem | fznn 13632 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
| ⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁))) | ||
| Theorem | elfz1b 13633 | Membership in a 1-based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) (Proof shortened by AV, 23-Jan-2022.) |
| ⊢ (𝑁 ∈ (1...𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ≤ 𝑀)) | ||
| Theorem | elfz1uz 13634 | Membership in a 1-based finite set of sequential integers with an upper integer. (Contributed by AV, 23-Jan-2022.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (1...𝑀)) | ||
| Theorem | elfzm11 13635 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) | ||
| Theorem | uzsplit 13636 | Express an upper integer set as the disjoint (see uzdisj 13637) union of the first 𝑁 values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑀) = ((𝑀...(𝑁 − 1)) ∪ (ℤ≥‘𝑁))) | ||
| Theorem | uzdisj 13637 | The first 𝑁 elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
| ⊢ ((𝑀...(𝑁 − 1)) ∩ (ℤ≥‘𝑁)) = ∅ | ||
| Theorem | fseq1p1m1 13638 | Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 7-Mar-2014.) |
| ⊢ 𝐻 = {〈(𝑁 + 1), 𝐵〉} ⇒ ⊢ (𝑁 ∈ ℕ0 → ((𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻)) ↔ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁))))) | ||
| Theorem | fseq1m1p1 13639 | Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.) |
| ⊢ 𝐻 = {〈𝑁, 𝐵〉} ⇒ ⊢ (𝑁 ∈ ℕ → ((𝐹:(1...(𝑁 − 1))⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻)) ↔ (𝐺:(1...𝑁)⟶𝐴 ∧ (𝐺‘𝑁) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...(𝑁 − 1)))))) | ||
| Theorem | fz1sbc 13640* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
| ⊢ (𝑁 ∈ ℤ → (∀𝑘 ∈ (𝑁...𝑁)𝜑 ↔ [𝑁 / 𝑘]𝜑)) | ||
| Theorem | elfzp1b 13641 | An integer is a member of a 0-based finite set of sequential integers iff its successor is a member of the corresponding 1-based set. (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...(𝑁 − 1)) ↔ (𝐾 + 1) ∈ (1...𝑁))) | ||
| Theorem | elfzm1b 13642 | An integer is a member of a 1-based finite set of sequential integers iff its predecessor is a member of the corresponding 0-based set. (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (1...𝑁) ↔ (𝐾 − 1) ∈ (0...(𝑁 − 1)))) | ||
| Theorem | elfzp12 13643 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁)))) | ||
| Theorem | fzne1 13644 | Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
| ⊢ ((𝐾 ∈ (𝑀...𝑁) ∧ 𝐾 ≠ 𝑀) → 𝐾 ∈ ((𝑀 + 1)...𝑁)) | ||
| Theorem | fzdif1 13645 | Split the first element of a finite set of sequential integers. More generic than fzpred 13612. Analogous to fzdif2 32792. (Contributed by AV, 12-Sep-2025.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁)) | ||
| Theorem | fz0dif1 13646 | Split the first element of a finite set of sequential nonnegative integers. (Contributed by AV, 12-Sep-2025.) |
| ⊢ (𝑁 ∈ ℕ0 → ((0...𝑁) ∖ {0}) = (1...𝑁)) | ||
| Theorem | fzm1 13647 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) | ||
| Theorem | fzneuz 13648 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → ¬ (𝑀...𝑁) = (ℤ≥‘𝐾)) | ||
| Theorem | fznuz 13649 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 30-Jun-2013.) (Revised by Mario Carneiro, 24-Aug-2013.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → ¬ 𝐾 ∈ (ℤ≥‘(𝑁 + 1))) | ||
| Theorem | uznfz 13650 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
| ⊢ (𝐾 ∈ (ℤ≥‘𝑁) → ¬ 𝐾 ∈ (𝑀...(𝑁 − 1))) | ||
| Theorem | fzp1nel 13651 | One plus the upper bound of a finite set of integers is not a member of that set. (Contributed by Scott Fenton, 16-Dec-2017.) |
| ⊢ ¬ (𝑁 + 1) ∈ (𝑀...𝑁) | ||
| Theorem | fzrevral 13652* | Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))[(𝐾 − 𝑘) / 𝑗]𝜑)) | ||
| Theorem | fzrevral2 13653* | Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[(𝐾 − 𝑘) / 𝑗]𝜑)) | ||
| Theorem | fzrevral3 13654* | Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[((𝑀 + 𝑁) − 𝑘) / 𝑗]𝜑)) | ||
| Theorem | fzshftral 13655* | Shift the scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) | ||
| Theorem | ige2m1fz1 13656 | Membership of an integer greater than 1 decreased by 1 in a 1-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.) |
| ⊢ (𝑁 ∈ (ℤ≥‘2) → (𝑁 − 1) ∈ (1...𝑁)) | ||
| Theorem | ige2m1fz 13657 | Membership in a 0-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 18-Jun-2018.) (Proof shortened by Alexander van der Vekens, 15-Sep-2018.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ (0...𝑁)) | ||
Finite intervals of nonnegative integers (or "finite sets of sequential nonnegative integers") are finite intervals of integers with 0 as lower bound: (0...𝑁), usually abbreviated by "fz0". | ||
| Theorem | elfz2nn0 13658 | Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁)) | ||
| Theorem | fznn0 13659 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁))) | ||
| Theorem | elfznn0 13660 | A member of a finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by NM, 5-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0) | ||
| Theorem | elfz3nn0 13661 | The upper bound of a nonempty finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ ℕ0) | ||
| Theorem | fz0ssnn0 13662 | Finite sets of sequential nonnegative integers starting with 0 are subsets of NN0. (Contributed by JJ, 1-Jun-2021.) |
| ⊢ (0...𝑁) ⊆ ℕ0 | ||
| Theorem | fz1ssfz0 13663 | Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| ⊢ (1...𝑁) ⊆ (0...𝑁) | ||
| Theorem | 0elfz 13664 | 0 is an element of a finite set of sequential nonnegative integers with a nonnegative integer as upper bound. (Contributed by AV, 6-Apr-2018.) |
| ⊢ (𝑁 ∈ ℕ0 → 0 ∈ (0...𝑁)) | ||
| Theorem | nn0fz0 13665 | A nonnegative integer is always part of the finite set of sequential nonnegative integers with this integer as upper bound. (Contributed by Scott Fenton, 21-Mar-2018.) |
| ⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (0...𝑁)) | ||
| Theorem | elfz0add 13666 | An element of a finite set of sequential nonnegative integers is an element of an extended finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝑁 ∈ (0...𝐴) → 𝑁 ∈ (0...(𝐴 + 𝐵)))) | ||
| Theorem | fz0sn 13667 | An integer range from 0 to 0 is a singleton. (Contributed by AV, 18-Apr-2021.) |
| ⊢ (0...0) = {0} | ||
| Theorem | fz0tp 13668 | An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
| ⊢ (0...2) = {0, 1, 2} | ||
| Theorem | fz0to3un2pr 13669 | An integer range from 0 to 3 is the union of two unordered pairs. (Contributed by AV, 7-Feb-2021.) |
| ⊢ (0...3) = ({0, 1} ∪ {2, 3}) | ||
| Theorem | fz0to4untppr 13670 | An integer range from 0 to 4 is the union of a triple and a pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Proof shortened by AV, 7-Aug-2025.) |
| ⊢ (0...4) = ({0, 1, 2} ∪ {3, 4}) | ||
| Theorem | fz0to5un2tp 13671 | An integer range from 0 to 5 is the union of two triples. (Contributed by AV, 30-Jul-2025.) |
| ⊢ (0...5) = ({0, 1, 2} ∪ {3, 4, 5}) | ||
| Theorem | elfz0ubfz0 13672 | An element of a finite set of sequential nonnegative integers is an element of a finite set of sequential nonnegative integers with the upper bound being an element of the finite set of sequential nonnegative integers with the same lower bound as for the first interval and the element under consideration as upper bound. (Contributed by Alexander van der Vekens, 3-Apr-2018.) |
| ⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → 𝐾 ∈ (0...𝐿)) | ||
| Theorem | elfz0fzfz0 13673 | A member of a finite set of sequential nonnegative integers is a member of a finite set of sequential nonnegative integers with a member of a finite set of sequential nonnegative integers starting at the upper bound of the first interval. (Contributed by Alexander van der Vekens, 27-May-2018.) |
| ⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → 𝑀 ∈ (0...𝑁)) | ||
| Theorem | fz0fzelfz0 13674 | If a member of a finite set of sequential integers with a lower bound being a member of a finite set of sequential nonnegative integers with the same upper bound, this member is also a member of the finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 21-Apr-2018.) |
| ⊢ ((𝑁 ∈ (0...𝑅) ∧ 𝑀 ∈ (𝑁...𝑅)) → 𝑀 ∈ (0...𝑅)) | ||
| Theorem | fznn0sub2 13675 | Subtraction closure for a member of a finite set of sequential nonnegative integers. (Contributed by NM, 26-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈ (0...𝑁)) | ||
| Theorem | uzsubfz0 13676 | Membership of an integer greater than L decreased by L in a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 16-Sep-2018.) |
| ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝐿)) → (𝑁 − 𝐿) ∈ (0...𝑁)) | ||
| Theorem | fz0fzdiffz0 13677 | The difference of an integer in a finite set of sequential nonnegative integers and and an integer of a finite set of sequential integers with the same upper bound and the nonnegative integer as lower bound is a member of the finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 6-Jun-2018.) |
| ⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐾 − 𝑀) ∈ (0...𝑁)) | ||
| Theorem | elfzmlbm 13678 | Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → (𝐾 − 𝑀) ∈ (0...(𝑁 − 𝑀))) | ||
| Theorem | elfzmlbp 13679 | Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) |
| ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ (𝑀...(𝑀 + 𝑁))) → (𝐾 − 𝑀) ∈ (0...𝑁)) | ||
| Theorem | fzctr 13680 | Lemma for theorems about the central binomial coefficient. (Contributed by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 2-Aug-2014.) |
| ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0...(2 · 𝑁))) | ||
| Theorem | difelfzle 13681 | The difference of two integers from a finite set of sequential nonnegative integers is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018.) |
| ⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝑀 ∈ (0...𝑁) ∧ 𝐾 ≤ 𝑀) → (𝑀 − 𝐾) ∈ (0...𝑁)) | ||
| Theorem | difelfznle 13682 | The difference of two integers from a finite set of sequential nonnegative integers increased by the upper bound is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018.) |
| ⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝑀 ∈ (0...𝑁) ∧ ¬ 𝐾 ≤ 𝑀) → ((𝑀 + 𝑁) − 𝐾) ∈ (0...𝑁)) | ||
| Theorem | nn0split 13683 | Express the set of nonnegative integers as the disjoint (see nn0disj 13684) union of the first 𝑁 + 1 values and the rest. (Contributed by AV, 8-Nov-2019.) |
| ⊢ (𝑁 ∈ ℕ0 → ℕ0 = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) | ||
| Theorem | nn0disj 13684 | The first 𝑁 + 1 elements of the set of nonnegative integers are distinct from any later members. (Contributed by AV, 8-Nov-2019.) |
| ⊢ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ | ||
| Theorem | fz0sn0fz1 13685 | A finite set of sequential nonnegative integers is the union of the singleton containing 0 and a finite set of sequential positive integers. (Contributed by AV, 20-Mar-2021.) |
| ⊢ (𝑁 ∈ ℕ0 → (0...𝑁) = ({0} ∪ (1...𝑁))) | ||
| Theorem | fvffz0 13686 | The function value of a function from a finite interval of nonnegative integers. (Contributed by AV, 13-Feb-2021.) |
| ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁) ∧ 𝑃:(0...𝑁)⟶𝑉) → (𝑃‘𝐼) ∈ 𝑉) | ||
| Theorem | 1fv 13687 | A function on a singleton. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Proof shortened by AV, 18-Apr-2021.) |
| ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑃 = {〈0, 𝑁〉}) → (𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁)) | ||
| Theorem | 4fvwrd4 13688* | The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |
| ⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑))) | ||
| Theorem | 2ffzeq 13689* | Two functions over 0-based finite set of sequential integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐹:(0...𝑀)⟶𝑋 ∧ 𝑃:(0...𝑁)⟶𝑌) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0...𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) | ||
| Theorem | preduz 13690 | The value of the predecessor class over an upper integer set. (Contributed by Scott Fenton, 16-May-2014.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → Pred( < , (ℤ≥‘𝑀), 𝑁) = (𝑀...(𝑁 − 1))) | ||
| Theorem | prednn 13691 | The value of the predecessor class over the naturals. (Contributed by Scott Fenton, 6-Aug-2013.) |
| ⊢ (𝑁 ∈ ℕ → Pred( < , ℕ, 𝑁) = (1...(𝑁 − 1))) | ||
| Theorem | prednn0 13692 | The value of the predecessor class over ℕ0. (Contributed by Scott Fenton, 9-May-2014.) |
| ⊢ (𝑁 ∈ ℕ0 → Pred( < , ℕ0, 𝑁) = (0...(𝑁 − 1))) | ||
| Theorem | predfz 13693 | Calculate the predecessor of an integer under a finite set of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
| ⊢ (𝐾 ∈ (𝑀...𝑁) → Pred( < , (𝑀...𝑁), 𝐾) = (𝑀...(𝐾 − 1))) | ||
| Syntax | cfzo 13694 | Syntax for half-open integer ranges. |
| class ..^ | ||
| Definition | df-fzo 13695* | Define a function generating sets of integers using a half-open range. Read (𝑀..^𝑁) as the integers from 𝑀 up to, but not including, 𝑁; contrast with (𝑀...𝑁) df-fz 13548, which includes 𝑁. Not including the endpoint simplifies a number of formulas related to cardinality and splitting; contrast fzosplit 13732 with fzsplit 13590, for instance. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
| ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1))) | ||
| Theorem | fzof 13696 | Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
| ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ | ||
| Theorem | elfzoel1 13697 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
| ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ) | ||
| Theorem | elfzoel2 13698 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
| ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ) | ||
| Theorem | elfzoelz 13699 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
| ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ) | ||
| Theorem | fzoval 13700 | Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
| ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |