Home | Intuitionistic Logic Explorer Theorem List (p. 91 of 105) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elfzubelfz 9001 | 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 9002 | A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.) |
Theorem | fzm 9003* | Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.) |
Theorem | fztri3or 9004 | Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
Theorem | fzdcel 9005 | Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
DECID | ||
Theorem | fznlem 9006 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.) |
Theorem | fzn 9007 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.) |
Theorem | fzen 9008 | A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.) |
Theorem | fz1n 9009 | A 1-based finite set of sequential integers is empty iff it ends at index . (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | 0fz1 9010 | Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.) |
Theorem | fz10 9011 | There are no integers between 1 and 0. (Contributed by Jeff Madsen, 16-Jun-2010.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
Theorem | uzsubsubfz 9012 | 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 9013 | 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.) |
Theorem | ige3m2fz 9014 | 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.) |
Theorem | fzsplit2 9015 | Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
Theorem | fzsplit 9016 | Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 13-Apr-2016.) |
Theorem | fzdisj 9017 | Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.) |
Theorem | fz01en 9018 | 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.) |
Theorem | elfznn 9019 | A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005.) |
Theorem | elfz1end 9020 | A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Theorem | fznn0sub 9021 | 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.) |
Theorem | fzmmmeqm 9022 | 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 9023 | Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
Theorem | fzsubel 9024 | Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
Theorem | fzopth 9025 | A finite set of sequential integers can represent an ordered pair. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzass4 9026 | Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
Theorem | fzss1 9027 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzss2 9028 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.) |
Theorem | fzssuz 9029 | A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
Theorem | fzsn 9030 | A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fzssp1 9031 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzsuc 9032 | 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.) |
Theorem | fzpred 9033 | Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
Theorem | fzpreddisj 9034 | A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.) |
Theorem | elfzp1 9035 | Append an element to a finite set of sequential integers. (Contributed by NM, 19-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzp1ss 9036 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzelp1 9037 | Membership in a set of sequential integers with an appended element. (Contributed by NM, 7-Dec-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzp1elp1 9038 | 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.) |
Theorem | fznatpl1 9039 | Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.) |
Theorem | fzpr 9040 | A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fztp 9041 | A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 7-Mar-2014.) |
Theorem | fzsuc2 9042 | Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014.) |
Theorem | fzp1disj 9043 | is the disjoint union of with . (Contributed by Mario Carneiro, 7-Mar-2014.) |
Theorem | fzdifsuc 9044 | Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.) |
Theorem | fzprval 9045* | Two ways of defining the first two values of a sequence on . (Contributed by NM, 5-Sep-2011.) |
Theorem | fztpval 9046* | Two ways of defining the first three values of a sequence on . (Contributed by NM, 13-Sep-2011.) |
Theorem | fzrev 9047 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev2 9048 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev2i 9049 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev3 9050 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fzrev3i 9051 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fznn 9052 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
Theorem | elfz1b 9053 | Membership in a 1 based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) |
Theorem | elfzm11 9054 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | uzsplit 9055 | Express an upper integer set as the disjoint (see uzdisj 9056) union of the first values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
Theorem | uzdisj 9056 | The first elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
Theorem | fseq1p1m1 9057 | 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.) |
Theorem | fseq1m1p1 9058 | Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | fz1sbc 9059* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
Theorem | elfzp1b 9060 | 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.) |
Theorem | elfzm1b 9061 | 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.) |
Theorem | elfzp12 9062 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
Theorem | fzm1 9063 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fzneuz 9064 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
Theorem | fznuz 9065 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 30-Jun-2013.) (Revised by Mario Carneiro, 24-Aug-2013.) |
Theorem | uznfz 9066 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
Theorem | fzp1nel 9067 | 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.) |
Theorem | fzrevral 9068* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrevral2 9069* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrevral3 9070* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fzshftral 9071* | Shift the scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
Theorem | ige2m1fz1 9072 | 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.) |
Theorem | ige2m1fz 9073 | 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.) |
Finite intervals of nonnegative integers (or "finite sets of sequential nonnegative integers") are finite intervals of integers with 0 as lower bound: , usually abbreviated by "fz0". | ||
Theorem | elfz2nn0 9074 | Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fznn0 9075 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
Theorem | elfznn0 9076 | 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.) |
Theorem | elfz3nn0 9077 | 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.) |
Theorem | 0elfz 9078 | 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.) |
Theorem | nn0fz0 9079 | 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.) |
Theorem | elfz0add 9080 | 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.) |
Theorem | elfz0addOLD 9081 | 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 9080 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | fz0tp 9082 | An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
Theorem | elfz0ubfz0 9083 | 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.) |
Theorem | elfz0fzfz0 9084 | 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.) |
Theorem | fz0fzelfz0 9085 | 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.) |
Theorem | fznn0sub2 9086 | 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.) |
Theorem | uzsubfz0 9087 | 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.) |
Theorem | fz0fzdiffz0 9088 | 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.) |
Theorem | elfzmlbm 9089 | 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.) |
Theorem | elfzmlbmOLD 9090 | 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 9089 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | elfzmlbp 9091 | 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.) |
Theorem | fzctr 9092 | Lemma for theorems about the central binomial coefficient. (Contributed by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 2-Aug-2014.) |
Theorem | difelfzle 9093 | 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.) |
Theorem | difelfznle 9094 | 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.) |
Theorem | nn0split 9095 | Express the set of nonnegative integers as the disjoint (see nn0disj 9096) union of the first values and the rest. (Contributed by AV, 8-Nov-2019.) |
Theorem | nn0disj 9096 | The first elements of the set of nonnegative integers are distinct from any later members. (Contributed by AV, 8-Nov-2019.) |
Theorem | 1fv 9097 | A one value function. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
Theorem | 4fvwrd4 9098* | The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |
Theorem | 2ffzeq 9099* | 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.) |
Syntax | cfzo 9100 | Syntax for half-open integer ranges. |
..^ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |