Home | Metamath
Proof Explorer Theorem List (p. 130 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elfzel1 12901 | 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 12902 | A member of a finite set of sequential integer is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ) | ||
Theorem | fzssz 12903 | A finite sequence of integers is a set of integers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝑀...𝑁) ⊆ ℤ | ||
Theorem | elfzle1 12904 | 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 12905 | 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 12906 | 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 12907 | 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 12908 | 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 12909 | 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 12910 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑁 ∈ (𝑀...𝑁)) | ||
Theorem | elfz3 12911 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (𝑁...𝑁)) | ||
Theorem | elfz1eq 12912 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.) |
⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁) | ||
Theorem | elfzubelfz 12913 | 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 12914 | 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 12915 | 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 12916 | A finite set of sequential integers is empty if its bounds are not integers. (Contributed by AV, 13-Oct-2018.) |
⊢ ((𝑀 ∉ ℤ ∨ 𝑁 ∉ ℤ) → (𝑀...𝑁) = ∅) | ||
Theorem | fzn 12917 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅)) | ||
Theorem | fzen 12918 | A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) | ||
Theorem | fz1n 12919 | 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 12920 | 0 is not an element of a finite interval of integers starting at 1. (Contributed by AV, 27-Aug-2020.) |
⊢ 0 ∉ (1...𝑁) | ||
Theorem | 0fz1 12921 | Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (1...𝑁)) → (𝐹 = ∅ ↔ 𝑁 = 0)) | ||
Theorem | fz10 12922 | 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 12923 | 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 12924 | 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 12925 | 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 12926 | Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁))) | ||
Theorem | fzsplit 12927 | 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 12928 | Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.) |
⊢ (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅) | ||
Theorem | fz01en 12929 | 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.) |
⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁)) | ||
Theorem | elfznn 12930 | 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 12931 | A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴)) | ||
Theorem | fz1ssnn 12932 | A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (1...𝐴) ⊆ ℕ | ||
Theorem | fznn0sub 12933 | 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 12934 | 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 12935 | Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) | ||
Theorem | fzadd2 12936 | Membership of a sum in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ)) → ((𝐽 ∈ (𝑀...𝑁) ∧ 𝐾 ∈ (𝑂...𝑃)) → (𝐽 + 𝐾) ∈ ((𝑀 + 𝑂)...(𝑁 + 𝑃)))) | ||
Theorem | fzsubel 12937 | Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾)))) | ||
Theorem | fzopth 12938 | A finite set of sequential integers has the ordered pair property (compare opth 5360) under certain conditions. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾))) | ||
Theorem | fzass4 12939 | Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐵 ∈ (𝐴...𝐷) ∧ 𝐶 ∈ (𝐵...𝐷)) ↔ (𝐵 ∈ (𝐴...𝐶) ∧ 𝐶 ∈ (𝐴...𝐷))) | ||
Theorem | fzss1 12940 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) | ||
Theorem | fzss2 12941 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁)) | ||
Theorem | fzssuz 12942 | A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀) | ||
Theorem | fzsn 12943 | A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) | ||
Theorem | fzssp1 12944 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1)) | ||
Theorem | fzssnn 12945 | 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 12946 | 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 12947 | 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 12948 | 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 12949 | Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) | ||
Theorem | fzpreddisj 12950 | A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ({𝑀} ∩ ((𝑀 + 1)...𝑁)) = ∅) | ||
Theorem | elfzp1 12951 | 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 12952 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) | ||
Theorem | fzelp1 12953 | 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 12954 | 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 12955 | Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁)) | ||
Theorem | fzpr 12956 | A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)}) | ||
Theorem | fztp 12957 | 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 12958 | An integer range between 1 and 2 is a pair. (Contributed by AV, 11-Jan-2023.) |
⊢ (1...2) = {1, 2} | ||
Theorem | fzsuc2 12959 | 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 12960 | (𝑀...(𝑁 + 1)) is the disjoint union of (𝑀...𝑁) with {(𝑁 + 1)}. (Contributed by Mario Carneiro, 7-Mar-2014.) |
⊢ ((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅ | ||
Theorem | fzdifsuc 12961 | Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) | ||
Theorem | fzprval 12962* | 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 12963* | 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 12964 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)) ↔ (𝐽 − 𝐾) ∈ (𝑀...𝑁))) | ||
Theorem | fzrev2 12965 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)))) | ||
Theorem | fzrev2i 12966 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀))) | ||
Theorem | fzrev3 12967 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ (𝐾 ∈ ℤ → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁))) | ||
Theorem | fzrev3i 12968 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁)) | ||
Theorem | fznn 12969 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfz1b 12970 | 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 12971 | Membership in a 1-based finite set of sequential integers with an upper integer. (Contributed by AV, 23-Jan-2022.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (1...𝑀)) | ||
Theorem | elfzm11 12972 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) | ||
Theorem | uzsplit 12973 | Express an upper integer set as the disjoint (see uzdisj 12974) union of the first 𝑁 values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑀) = ((𝑀...(𝑁 − 1)) ∪ (ℤ≥‘𝑁))) | ||
Theorem | uzdisj 12974 | The first 𝑁 elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ ((𝑀...(𝑁 − 1)) ∩ (ℤ≥‘𝑁)) = ∅ | ||
Theorem | fseq1p1m1 12975 | 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 12976 | 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 12977* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
⊢ (𝑁 ∈ ℤ → (∀𝑘 ∈ (𝑁...𝑁)𝜑 ↔ [𝑁 / 𝑘]𝜑)) | ||
Theorem | elfzp1b 12978 | 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 12979 | 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 12980 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁)))) | ||
Theorem | fzm1 12981 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) | ||
Theorem | fzneuz 12982 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → ¬ (𝑀...𝑁) = (ℤ≥‘𝐾)) | ||
Theorem | fznuz 12983 | 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 12984 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
⊢ (𝐾 ∈ (ℤ≥‘𝑁) → ¬ 𝐾 ∈ (𝑀...(𝑁 − 1))) | ||
Theorem | fzp1nel 12985 | 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 12986* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))[(𝐾 − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzrevral2 12987* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[(𝐾 − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzrevral3 12988* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[((𝑀 + 𝑁) − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzshftral 12989* | Shift the scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) | ||
Theorem | ige2m1fz1 12990 | 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 12991 | 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 12992 | 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 12993 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
⊢ (𝑁 ∈ ℕ0 → (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfznn0 12994 | 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 12995 | 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 12996 | Finite sets of sequential nonnegative integers starting with 0 are subsets of NN0. (Contributed by JJ, 1-Jun-2021.) |
⊢ (0...𝑁) ⊆ ℕ0 | ||
Theorem | fz1ssfz0 12997 | Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (1...𝑁) ⊆ (0...𝑁) | ||
Theorem | 0elfz 12998 | 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 12999 | 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 13000 | 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...(𝐴 + 𝐵)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |