Home | Intuitionistic Logic Explorer Theorem List (p. 100 of 139) | < 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 | dfioo2 9901* | Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro, 1-Sep-2015.) |
Theorem | ioorebasg 9902 | Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.) |
Theorem | elrege0 9903 | The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) |
Theorem | rge0ssre 9904 | Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.) |
Theorem | elxrge0 9905 | Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
Theorem | 0e0icopnf 9906 | 0 is a member of (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 0e0iccpnf 9907 | 0 is a member of (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | ge0addcl 9908 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.) |
Theorem | ge0mulcl 9909 | The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.) |
Theorem | ge0xaddcl 9910 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.) |
Theorem | lbicc2 9911 | The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) (Revised by Mario Carneiro, 9-Sep-2015.) |
Theorem | ubicc2 9912 | The upper bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) |
Theorem | 0elunit 9913 | Zero is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.) |
Theorem | 1elunit 9914 | One is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.) |
Theorem | iooneg 9915 | Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
Theorem | iccneg 9916 | Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
Theorem | icoshft 9917 | A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.) |
Theorem | icoshftf1o 9918* | Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
Theorem | icodisj 9919 | End-to-end closed-below, open-above real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.) |
Theorem | ioodisj 9920 | If the upper bound of one open interval is less than or equal to the lower bound of the other, the intervals are disjoint. (Contributed by Jeff Hankins, 13-Jul-2009.) |
Theorem | iccshftr 9921 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iccshftri 9922 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iccshftl 9923 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iccshftli 9924 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iccdil 9925 | Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iccdili 9926 | Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | icccntr 9927 | Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | icccntri 9928 | Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | divelunit 9929 | A condition for a ratio to be a member of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.) |
Theorem | lincmb01cmp 9930 | A linear combination of two reals which lies in the interval between them. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 8-Sep-2015.) |
Theorem | iccf1o 9931* | Describe a bijection from to an arbitrary nontrivial closed interval . (Contributed by Mario Carneiro, 8-Sep-2015.) |
Theorem | unitssre 9932 | is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | iccen 9933 | Any nontrivial closed interval is equinumerous to the unit interval. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 8-Sep-2015.) |
Theorem | zltaddlt1le 9934 | The sum of an integer and a real number between 0 and 1 is less than or equal to a second integer iff the sum is less than the second integer. (Contributed by AV, 1-Jul-2021.) |
Syntax | cfz 9935 |
Extend class notation to include the notation for a contiguous finite set
of integers. Read " " as "the set of
integers from to
inclusive".
This symbol is also used informally in some comments to denote an ellipsis, e.g., . |
Definition | df-fz 9936* | Define an operation that produces a finite set of sequential integers. Read " " as "the set of integers from to inclusive." See fzval 9937 for its value and additional comments. (Contributed by NM, 6-Sep-2005.) |
Theorem | fzval 9937* | The value of a finite set of sequential integers. E.g., means the set . A special case of this definition (starting at 1) appears as Definition 11-2.1 of [Gleason] p. 141, where k means our ; he calls these sets segments of the integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Theorem | fzval2 9938 | An alternate way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.) |
Theorem | fzf 9939 | 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 9940 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) |
Theorem | elfz 9941 | Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.) |
Theorem | elfz2 9942 | 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 9943 | Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.) |
Theorem | elfz4 9944 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | elfzuzb 9945 | 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 9946 | Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | elfzuz 9947 | 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 9948 | 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 9949 | 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 9950 | 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 9951 | 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 9952 | 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 9953 | 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 9954 | 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 9955 | 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 9956 | 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 9957 | 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 9958 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.) |
Theorem | elfz3 9959 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.) |
Theorem | elfz1eq 9960 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.) |
Theorem | elfzubelfz 9961 | 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 9962 | A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.) |
Theorem | fzm 9963* | Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.) |
Theorem | fztri3or 9964 | Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
Theorem | fzdcel 9965 | Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
DECID | ||
Theorem | fznlem 9966 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.) |
Theorem | fzn 9967 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.) |
Theorem | fzen 9968 | A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.) |
Theorem | fz1n 9969 | A 1-based finite set of sequential integers is empty iff it ends at index . (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | 0fz1 9970 | Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.) |
Theorem | fz10 9971 | 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 9972 | 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 9973 | 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 9974 | 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 9975 | Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
Theorem | fzsplit 9976 | 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 9977 | Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.) |
Theorem | fz01en 9978 | 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.) |
Theorem | elfznn 9979 | A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005.) |
Theorem | elfz1end 9980 | A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Theorem | fz1ssnn 9981 | A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
Theorem | fznn0sub 9982 | 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 9983 | 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 9984 | Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
Theorem | fzsubel 9985 | Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
Theorem | fzopth 9986 | 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 9987 | Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
Theorem | fzss1 9988 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzss2 9989 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.) |
Theorem | fzssuz 9990 | A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
Theorem | fzsn 9991 | A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fzssp1 9992 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzssnn 9993 | 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 9994 | 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 9995 | Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
Theorem | fzpreddisj 9996 | A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.) |
Theorem | elfzp1 9997 | 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 9998 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fzelp1 9999 | 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 10000 | 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.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |