Home | Intuitionistic Logic Explorer Theorem List (p. 100 of 135) | < 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 | fzopth 9901 | 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 9902 | Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
Theorem | fzss1 9903 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzss2 9904 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.) |
Theorem | fzssuz 9905 | A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
Theorem | fzsn 9906 | A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fzssp1 9907 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzssnn 9908 | 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 9909 | 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 9910 | Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
Theorem | fzpreddisj 9911 | A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.) |
Theorem | elfzp1 9912 | 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 9913 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzelp1 9914 | 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 9915 | 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 9916 | Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.) |
Theorem | fzpr 9917 | A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fztp 9918 | A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 7-Mar-2014.) |
Theorem | fzsuc2 9919 | Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014.) |
Theorem | fzp1disj 9920 | is the disjoint union of with . (Contributed by Mario Carneiro, 7-Mar-2014.) |
Theorem | fzdifsuc 9921 | Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.) |
Theorem | fzprval 9922* | Two ways of defining the first two values of a sequence on . (Contributed by NM, 5-Sep-2011.) |
Theorem | fztpval 9923* | Two ways of defining the first three values of a sequence on . (Contributed by NM, 13-Sep-2011.) |
Theorem | fzrev 9924 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev2 9925 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev2i 9926 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev3 9927 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fzrev3i 9928 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fznn 9929 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
Theorem | elfz1b 9930 | Membership in a 1 based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) |
Theorem | elfzm11 9931 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | uzsplit 9932 | Express an upper integer set as the disjoint (see uzdisj 9933) union of the first values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
Theorem | uzdisj 9933 | The first elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
Theorem | fseq1p1m1 9934 | 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 9935 | Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | fz1sbc 9936* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
Theorem | elfzp1b 9937 | 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 9938 | 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 9939 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
Theorem | fzm1 9940 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fzneuz 9941 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
Theorem | fznuz 9942 | 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 9943 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
Theorem | fzp1nel 9944 | 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 9945* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrevral2 9946* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrevral3 9947* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fzshftral 9948* | Shift the scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
Theorem | ige2m1fz1 9949 | 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 9950 | 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 9951 | 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 9952 | Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fznn0 9953 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
Theorem | elfznn0 9954 | 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 9955 | 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 | fz0ssnn0 9956 | Finite sets of sequential nonnegative integers starting with 0 are subsets of NN0. (Contributed by JJ, 1-Jun-2021.) |
Theorem | fz1ssfz0 9957 | Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Theorem | 0elfz 9958 | 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 9959 | 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 9960 | 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 | fz0tp 9961 | An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
Theorem | elfz0ubfz0 9962 | 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 9963 | 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 9964 | 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 9965 | 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 9966 | 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 9967 | 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 9968 | 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 | elfzmlbp 9969 | 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 9970 | Lemma for theorems about the central binomial coefficient. (Contributed by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 2-Aug-2014.) |
Theorem | difelfzle 9971 | 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 9972 | 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 9973 | Express the set of nonnegative integers as the disjoint (see nn0disj 9975) union of the first values and the rest. (Contributed by AV, 8-Nov-2019.) |
Theorem | nnsplit 9974 | Express the set of positive integers as the disjoint union of the first values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Theorem | nn0disj 9975 | The first elements of the set of nonnegative integers are distinct from any later members. (Contributed by AV, 8-Nov-2019.) |
Theorem | 1fv 9976 | A function on a singleton. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
Theorem | 4fvwrd4 9977* | The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |
Theorem | 2ffzeq 9978* | 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 9979 | Syntax for half-open integer ranges. |
..^ | ||
Definition | df-fzo 9980* | 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 9851, which includes . Not including the endpoint simplifies a number of formulas related to cardinality and splitting; contrast fzosplit 10014 with fzsplit 9891, for instance. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | fzof 9981 | Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | elfzoel1 9982 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | elfzoel2 9983 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | elfzoelz 9984 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | fzoval 9985 | Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | elfzo 9986 | Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
..^ | ||
Theorem | elfzo2 9987 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ | ||
Theorem | elfzouz 9988 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ | ||
Theorem | fzodcel 9989 | Decidability of membership in a half-open integer interval. (Contributed by Jim Kingdon, 25-Aug-2022.) |
DECID ..^ | ||
Theorem | fzolb 9990 | The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with . This provides an alternate notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate . (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ | ||
Theorem | fzolb2 9991 | The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with . This provides an alternate notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate . (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ | ||
Theorem | elfzole1 9992 | 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 9993 | A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
..^ | ||
Theorem | elfzolt3 9994 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
..^ | ||
Theorem | elfzolt2b 9995 | A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ ..^ | ||
Theorem | elfzolt3b 9996 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ ..^ | ||
Theorem | fzonel 9997 | A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
..^ | ||
Theorem | elfzouz2 9998 | 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 9999 | A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
..^ | ||
Theorem | elfzo3 10000 | 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.) |
..^ ..^ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |