Home | Intuitionistic Logic Explorer Theorem List (p. 90 of 100) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elfzp1 8901 | 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 8902 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) | ||
Theorem | fzelp1 8903 | 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 8904 | 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 8905 | Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁)) | ||
Theorem | fzpr 8906 | A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)}) | ||
Theorem | fztp 8907 | 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 | fzsuc2 8908 | 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 8909 | (𝑀...(𝑁 + 1)) is the disjoint union of (𝑀...𝑁) with {(𝑁 + 1)}. (Contributed by Mario Carneiro, 7-Mar-2014.) |
⊢ ((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅ | ||
Theorem | fzdifsuc 8910 | Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) | ||
Theorem | fzprval 8911* | 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 8912* | 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 8913 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)) ↔ (𝐽 − 𝐾) ∈ (𝑀...𝑁))) | ||
Theorem | fzrev2 8914 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)))) | ||
Theorem | fzrev2i 8915 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀))) | ||
Theorem | fzrev3 8916 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ (𝐾 ∈ ℤ → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁))) | ||
Theorem | fzrev3i 8917 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁)) | ||
Theorem | fznn 8918 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfz1b 8919 | Membership in a 1 based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) |
⊢ (𝑁 ∈ (1...𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ≤ 𝑀)) | ||
Theorem | elfzm11 8920 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) | ||
Theorem | uzsplit 8921 | Express an upper integer set as the disjoint (see uzdisj 8922) union of the first 𝑁 values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (ℤ_{≥}‘𝑀) = ((𝑀...(𝑁 − 1)) ∪ (ℤ_{≥}‘𝑁))) | ||
Theorem | uzdisj 8922 | The first 𝑁 elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ ((𝑀...(𝑁 − 1)) ∩ (ℤ_{≥}‘𝑁)) = ∅ | ||
Theorem | fseq1p1m1 8923 | 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 8924 | 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 8925* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
⊢ (𝑁 ∈ ℤ → (∀𝑘 ∈ (𝑁...𝑁)𝜑 ↔ [𝑁 / 𝑘]𝜑)) | ||
Theorem | elfzp1b 8926 | 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 8927 | 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 8928 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁)))) | ||
Theorem | fzm1 8929 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) | ||
Theorem | fzneuz 8930 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
⊢ ((𝑁 ∈ (ℤ_{≥}‘𝑀) ∧ 𝐾 ∈ ℤ) → ¬ (𝑀...𝑁) = (ℤ_{≥}‘𝐾)) | ||
Theorem | fznuz 8931 | 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 8932 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
⊢ (𝐾 ∈ (ℤ_{≥}‘𝑁) → ¬ 𝐾 ∈ (𝑀...(𝑁 − 1))) | ||
Theorem | fzp1nel 8933 | 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 8934* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))[(𝐾 − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzrevral2 8935* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[(𝐾 − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzrevral3 8936* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[((𝑀 + 𝑁) − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzshftral 8937* | Shift the scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) | ||
Theorem | ige2m1fz1 8938 | 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 8939 | 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 8940 | 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 8941 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
⊢ (𝑁 ∈ ℕ_{0} → (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ_{0} ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfznn0 8942 | 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 8943 | 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 | 0elfz 8944 | 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 8945 | 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 8946 | 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 | elfz0addOLD 8947 | 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.) Obsolete version of elfz0add 8946 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ ℕ_{0} ∧ 𝐵 ∈ ℕ_{0}) → (𝑁 ∈ (0...𝐴) → 𝑁 ∈ (0...(𝐴 + 𝐵)))) | ||
Theorem | fz0tp 8948 | 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 | elfz0ubfz0 8949 | 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 8950 | 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 8951 | 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 8952 | 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 8953 | 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 8954 | 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 8955 | 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 | elfzmlbmOLD 8956 | 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.) Obsolete version of elfzmlbm 8955 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝐾 − 𝑀) ∈ (0...(𝑁 − 𝑀))) | ||
Theorem | elfzmlbp 8957 | 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 8958 | 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 8959 | 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 8960 | 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 8961 | Express the set of nonnegative integers as the disjoint (see nn0disj 8962) union of the first 𝑁 + 1 values and the rest. (Contributed by AV, 8-Nov-2019.) |
⊢ (𝑁 ∈ ℕ_{0} → ℕ_{0} = ((0...𝑁) ∪ (ℤ_{≥}‘(𝑁 + 1)))) | ||
Theorem | nn0disj 8962 | 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 | 1fv 8963 | A one value function. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑃 = {⟨0, 𝑁⟩}) → (𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁)) | ||
Theorem | 4fvwrd4 8964* | 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 8965* | 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...𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) | ||
Syntax | cfzo 8966 | Syntax for half-open integer ranges. |
class ..^ | ||
Definition | df-fzo 8967* | 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 8842, which includes 𝑁. Not including the endpoint simplifies a number of formulae related to cardinality and splitting; contrast fzosplit 9000 with fzsplit 8882, for instance. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1))) | ||
Theorem | fzof 8968 | Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ | ||
Theorem | elfzoel1 8969 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ) | ||
Theorem | elfzoel2 8970 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ) | ||
Theorem | elfzoelz 8971 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ) | ||
Theorem | fzoval 8972 | Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) | ||
Theorem | elfzo 8973 | Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) | ||
Theorem | elfzo2 8974 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ_{≥}‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁)) | ||
Theorem | elfzouz 8975 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (ℤ_{≥}‘𝑀)) | ||
Theorem | fzolb 8976 | The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with 𝑀 < 𝑁. This provides an alternative notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate 𝑀 ∈ (ℤ_{≥}‘𝑁). (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)) | ||
Theorem | fzolb2 8977 | The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with 𝑀 < 𝑁. This provides an alternative notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate 𝑀 ∈ (ℤ_{≥}‘𝑁). (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (𝑀..^𝑁) ↔ 𝑀 < 𝑁)) | ||
Theorem | elfzole1 8978 | A member in a half-open integer interval is greater than or equal to the lower bound. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝐾) | ||
Theorem | elfzolt2 8979 | A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 < 𝑁) | ||
Theorem | elfzolt3 8980 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 < 𝑁) | ||
Theorem | elfzolt2b 8981 | A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝐾..^𝑁)) | ||
Theorem | elfzolt3b 8982 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 ∈ (𝑀..^𝑁)) | ||
Theorem | fzonel 8983 | A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ ¬ 𝐵 ∈ (𝐴..^𝐵) | ||
Theorem | elfzouz2 8984 | The upper bound of a half-open range is greater or equal to an element of the range. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑁 ∈ (ℤ_{≥}‘𝐾)) | ||
Theorem | elfzofz 8985 | A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝑀...𝑁)) | ||
Theorem | elfzo3 8986 | Express membership in a half-open integer interval in terms of the "less than or equal" and "less than" predicates on integers, resp. 𝐾 ∈ (ℤ_{≥}‘𝑀) ↔ 𝑀 ≤ 𝐾, 𝐾 ∈ (𝐾..^𝑁) ↔ 𝐾 < 𝑁. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ_{≥}‘𝑀) ∧ 𝐾 ∈ (𝐾..^𝑁))) | ||
Theorem | fzom 8987* | A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.) |
⊢ (∃𝑥 𝑥 ∈ (𝑀..^𝑁) ↔ 𝑀 ∈ (𝑀..^𝑁)) | ||
Theorem | fzossfz 8988 | A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐴..^𝐵) ⊆ (𝐴...𝐵) | ||
Theorem | fzon 8989 | A half-open set of sequential integers is empty if the bounds are equal or reversed. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅)) | ||
Theorem | fzonlt0 8990 | A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑀 < 𝑁 ↔ (𝑀..^𝑁) = ∅)) | ||
Theorem | fzo0 8991 | Half-open sets with equal endpoints are empty. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐴..^𝐴) = ∅ | ||
Theorem | fzonnsub 8992 | If 𝐾 < 𝑁 then 𝑁 − 𝐾 is a positive integer. (Contributed by Mario Carneiro, 29-Sep-2015.) (Revised by Mario Carneiro, 1-Jan-2017.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝐾) ∈ ℕ) | ||
Theorem | fzonnsub2 8993 | If 𝑀 < 𝑁 then 𝑁 − 𝑀 is a positive integer. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝑀) ∈ ℕ) | ||
Theorem | fzoss1 8994 | Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (ℤ_{≥}‘𝑀) → (𝐾..^𝑁) ⊆ (𝑀..^𝑁)) | ||
Theorem | fzoss2 8995 | Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝐾) → (𝑀..^𝐾) ⊆ (𝑀..^𝑁)) | ||
Theorem | fzossrbm1 8996 | Subset of a half open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
⊢ (𝑁 ∈ ℤ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) | ||
Theorem | fzo0ss1 8997 | Subset relationship for half-open integer ranges with lower bounds 0 and 1. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
⊢ (1..^𝑁) ⊆ (0..^𝑁) | ||
Theorem | fzossnn0 8998 | A half-open integer range starting at a nonnegative integer is a subset of the nonnegative integers. (Contributed by Alexander van der Vekens, 13-May-2018.) |
⊢ (𝑀 ∈ ℕ_{0} → (𝑀..^𝑁) ⊆ ℕ_{0}) | ||
Theorem | fzospliti 8999 | One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 ∈ (𝐵..^𝐷) ∨ 𝐴 ∈ (𝐷..^𝐶))) | ||
Theorem | fzosplit 9000 | Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐷 ∈ (𝐵...𝐶) → (𝐵..^𝐶) = ((𝐵..^𝐷) ∪ (𝐷..^𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |