Home | Intuitionistic Logic Explorer Theorem List (p. 99 of 133) | < 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 | fzf 9801 | 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 9802 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) |
Theorem | elfz 9803 | Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.) |
Theorem | elfz2 9804 | 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 | elfz5 9805 | Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.) |
Theorem | elfz4 9806 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | elfzuzb 9807 | 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 9808 | Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | elfzuz 9809 | 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 9810 | 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 9811 | 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 9812 | 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 9813 | 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 | elfzle1 9814 | 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 9815 | 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 9816 | 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 9817 | 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 9818 | 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 9819 | 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 9820 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.) |
Theorem | elfz3 9821 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.) |
Theorem | elfz1eq 9822 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.) |
Theorem | elfzubelfz 9823 | 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 9824 | A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.) |
Theorem | fzm 9825* | Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.) |
Theorem | fztri3or 9826 | Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
Theorem | fzdcel 9827 | Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
DECID | ||
Theorem | fznlem 9828 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.) |
Theorem | fzn 9829 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.) |
Theorem | fzen 9830 | A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.) |
Theorem | fz1n 9831 | A 1-based finite set of sequential integers is empty iff it ends at index . (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | 0fz1 9832 | Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.) |
Theorem | fz10 9833 | 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 9834 | 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 9835 | 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 9836 | 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 9837 | Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
Theorem | fzsplit 9838 | 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 9839 | Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.) |
Theorem | fz01en 9840 | 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.) |
Theorem | elfznn 9841 | A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005.) |
Theorem | elfz1end 9842 | A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Theorem | fz1ssnn 9843 | A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
Theorem | fznn0sub 9844 | 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 9845 | 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 9846 | Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
Theorem | fzsubel 9847 | Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
Theorem | fzopth 9848 | 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 9849 | Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
Theorem | fzss1 9850 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzss2 9851 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.) |
Theorem | fzssuz 9852 | A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
Theorem | fzsn 9853 | A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fzssp1 9854 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzssnn 9855 | Finite sets of sequential integers starting from a natural are a subset of the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
Theorem | fzsuc 9856 | 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 9857 | Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
Theorem | fzpreddisj 9858 | A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.) |
Theorem | elfzp1 9859 | 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 9860 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzelp1 9861 | 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 9862 | 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 9863 | Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.) |
Theorem | fzpr 9864 | A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fztp 9865 | A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 7-Mar-2014.) |
Theorem | fzsuc2 9866 | Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014.) |
Theorem | fzp1disj 9867 | is the disjoint union of with . (Contributed by Mario Carneiro, 7-Mar-2014.) |
Theorem | fzdifsuc 9868 | Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.) |
Theorem | fzprval 9869* | Two ways of defining the first two values of a sequence on . (Contributed by NM, 5-Sep-2011.) |
Theorem | fztpval 9870* | Two ways of defining the first three values of a sequence on . (Contributed by NM, 13-Sep-2011.) |
Theorem | fzrev 9871 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev2 9872 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev2i 9873 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev3 9874 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fzrev3i 9875 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fznn 9876 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
Theorem | elfz1b 9877 | Membership in a 1 based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) |
Theorem | elfzm11 9878 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | uzsplit 9879 | Express an upper integer set as the disjoint (see uzdisj 9880) union of the first values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
Theorem | uzdisj 9880 | The first elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
Theorem | fseq1p1m1 9881 | 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 9882 | Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | fz1sbc 9883* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
Theorem | elfzp1b 9884 | 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 9885 | 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 9886 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
Theorem | fzm1 9887 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fzneuz 9888 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
Theorem | fznuz 9889 | 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 9890 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
Theorem | fzp1nel 9891 | 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 9892* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrevral2 9893* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrevral3 9894* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fzshftral 9895* | Shift the scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
Theorem | ige2m1fz1 9896 | 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 9897 | 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.) |
Theorem | fz01or 9898 | An integer is in the integer range from zero to one iff it is either zero or one. (Contributed by Jim Kingdon, 11-Nov-2021.) |
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 9899 | Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fznn0 9900 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |