![]() |
Intuitionistic Logic Explorer Theorem List (p. 101 of 149) | < 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 | divelunit 10001 | A condition for a ratio to be a member of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ (π΅ β β β§ 0 < π΅)) β ((π΄ / π΅) β (0[,]1) β π΄ β€ π΅)) | ||
Theorem | lincmb01cmp 10002 | 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.) |
β’ (((π΄ β β β§ π΅ β β β§ π΄ < π΅) β§ π β (0[,]1)) β (((1 β π) Β· π΄) + (π Β· π΅)) β (π΄[,]π΅)) | ||
Theorem | iccf1o 10003* | Describe a bijection from [0, 1] to an arbitrary nontrivial closed interval [π΄, π΅]. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ πΉ = (π₯ β (0[,]1) β¦ ((π₯ Β· π΅) + ((1 β π₯) Β· π΄))) β β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β (πΉ:(0[,]1)β1-1-ontoβ(π΄[,]π΅) β§ β‘πΉ = (π¦ β (π΄[,]π΅) β¦ ((π¦ β π΄) / (π΅ β π΄))))) | ||
Theorem | unitssre 10004 | (0[,]1) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
β’ (0[,]1) β β | ||
Theorem | iccen 10005 | Any nontrivial closed interval is equinumerous to the unit interval. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 8-Sep-2015.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β (0[,]1) β (π΄[,]π΅)) | ||
Theorem | zltaddlt1le 10006 | 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.) |
β’ ((π β β€ β§ π β β€ β§ π΄ β (0(,)1)) β ((π + π΄) < π β (π + π΄) β€ π)) | ||
Syntax | cfz 10007 |
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., π΄ + π΄β2 + ... + π΄β(π β 1). |
class ... | ||
Definition | df-fz 10008* | Define an operation that produces a finite set of sequential integers. Read "π...π " as "the set of integers from π to π inclusive". See fzval 10009 for its value and additional comments. (Contributed by NM, 6-Sep-2005.) |
β’ ... = (π β β€, π β β€ β¦ {π β β€ β£ (π β€ π β§ π β€ π)}) | ||
Theorem | fzval 10009* | The value of a finite set of sequential integers. E.g., 2...5 means the set {2, 3, 4, 5}. A special case of this definition (starting at 1) appears as Definition 11-2.1 of [Gleason] p. 141, where βk means our 1...π; he calls these sets segments of the integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π β β€ β§ π β β€) β (π...π) = {π β β€ β£ (π β€ π β§ π β€ π)}) | ||
Theorem | fzval2 10010 | An alternate way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ ((π β β€ β§ π β β€) β (π...π) = ((π[,]π) β© β€)) | ||
Theorem | fzf 10011 | 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 10012 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) |
β’ ((π β β€ β§ π β β€) β (πΎ β (π...π) β (πΎ β β€ β§ π β€ πΎ β§ πΎ β€ π))) | ||
Theorem | elfz 10013 | Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (πΎ β (π...π) β (π β€ πΎ β§ πΎ β€ π))) | ||
Theorem | elfz2 10014 | 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 | elfzd 10015 | Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β π β€ πΎ) & β’ (π β πΎ β€ π) β β’ (π β πΎ β (π...π)) | ||
Theorem | elfz5 10016 | Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.) |
β’ ((πΎ β (β€β₯βπ) β§ π β β€) β (πΎ β (π...π) β πΎ β€ π)) | ||
Theorem | elfz4 10017 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (((π β β€ β§ π β β€ β§ πΎ β β€) β§ (π β€ πΎ β§ πΎ β€ π)) β πΎ β (π...π)) | ||
Theorem | elfzuzb 10018 | 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 10019 | Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ ((πΎ β (β€β₯βπ) β§ π β (β€β₯βπΎ)) β πΎ β (π...π)) | ||
Theorem | elfzuz 10020 | 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 10021 | 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 10022 | 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 10023 | 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 10024 | 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 | elfzelzd 10025 | A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β πΎ β (π...π)) β β’ (π β πΎ β β€) | ||
Theorem | elfzle1 10026 | 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 10027 | 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 10028 | 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 10029 | 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 10030 | 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 10031 | 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 10032 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.) |
β’ (π β (β€β₯βπ) β π β (π...π)) | ||
Theorem | elfz3 10033 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.) |
β’ (π β β€ β π β (π...π)) | ||
Theorem | elfz1eq 10034 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.) |
β’ (πΎ β (π...π) β πΎ = π) | ||
Theorem | elfzubelfz 10035 | 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 10036 | A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.) |
β’ ((πΎ β (β€β₯βπ) β§ (πΎ + 1) β (π...π)) β πΎ β (π...π)) | ||
Theorem | fzm 10037* | Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.) |
β’ (βπ₯ π₯ β (π...π) β π β (β€β₯βπ)) | ||
Theorem | fztri3or 10038 | Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (πΎ < π β¨ πΎ β (π...π) β¨ π < πΎ)) | ||
Theorem | fzdcel 10039 | Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β DECID πΎ β (π...π)) | ||
Theorem | fznlem 10040 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.) |
β’ ((π β β€ β§ π β β€) β (π < π β (π...π) = β )) | ||
Theorem | fzn 10041 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.) |
β’ ((π β β€ β§ π β β€) β (π < π β (π...π) = β )) | ||
Theorem | fzen 10042 | A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.) |
β’ ((π β β€ β§ π β β€ β§ πΎ β β€) β (π...π) β ((π + πΎ)...(π + πΎ))) | ||
Theorem | fz1n 10043 | A 1-based finite set of sequential integers is empty iff it ends at index 0. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ (π β β0 β ((1...π) = β β π = 0)) | ||
Theorem | 0fz1 10044 | Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.) |
β’ ((π β β0 β§ πΉ Fn (1...π)) β (πΉ = β β π = 0)) | ||
Theorem | fz10 10045 | There are no integers between 1 and 0. (Contributed by Jeff Madsen, 16-Jun-2010.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
β’ (1...0) = β | ||
Theorem | uzsubsubfz 10046 | 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 10047 | 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.) |
β’ ((πΏ β β β§ π β (β€β₯βπΏ)) β (π β (πΏ β 1)) β (1...π)) | ||
Theorem | ige3m2fz 10048 | 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.) |
β’ (π β (β€β₯β3) β (π β 2) β (1...π)) | ||
Theorem | fzsplit2 10049 | Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
β’ (((πΎ + 1) β (β€β₯βπ) β§ π β (β€β₯βπΎ)) β (π...π) = ((π...πΎ) βͺ ((πΎ + 1)...π))) | ||
Theorem | fzsplit 10050 | Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 13-Apr-2016.) |
β’ (πΎ β (π...π) β (π...π) = ((π...πΎ) βͺ ((πΎ + 1)...π))) | ||
Theorem | fzdisj 10051 | Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.) |
β’ (πΎ < π β ((π½...πΎ) β© (π...π)) = β ) | ||
Theorem | fz01en 10052 | 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.) |
β’ (π β β€ β (0...(π β 1)) β (1...π)) | ||
Theorem | elfznn 10053 | A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005.) |
β’ (πΎ β (1...π) β πΎ β β) | ||
Theorem | elfz1end 10054 | A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (π΄ β β β π΄ β (1...π΄)) | ||
Theorem | fz1ssnn 10055 | A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ (1...π΄) β β | ||
Theorem | fznn0sub 10056 | 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.) |
β’ (πΎ β (π...π) β (π β πΎ) β β0) | ||
Theorem | fzmmmeqm 10057 | 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 10058 | Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
β’ (((π β β€ β§ π β β€) β§ (π½ β β€ β§ πΎ β β€)) β (π½ β (π...π) β (π½ + πΎ) β ((π + πΎ)...(π + πΎ)))) | ||
Theorem | fzsubel 10059 | Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
β’ (((π β β€ β§ π β β€) β§ (π½ β β€ β§ πΎ β β€)) β (π½ β (π...π) β (π½ β πΎ) β ((π β πΎ)...(π β πΎ)))) | ||
Theorem | fzopth 10060 | 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 10061 | Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π΅ β (π΄...π·) β§ πΆ β (π΅...π·)) β (π΅ β (π΄...πΆ) β§ πΆ β (π΄...π·))) | ||
Theorem | fzss1 10062 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
β’ (πΎ β (β€β₯βπ) β (πΎ...π) β (π...π)) | ||
Theorem | fzss2 10063 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ (π β (β€β₯βπΎ) β (π...πΎ) β (π...π)) | ||
Theorem | fzssuz 10064 | A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
β’ (π...π) β (β€β₯βπ) | ||
Theorem | fzsn 10065 | A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β β€ β (π...π) = {π}) | ||
Theorem | fzssp1 10066 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (π...π) β (π...(π + 1)) | ||
Theorem | fzssnn 10067 | 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 10068 | 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.) |
β’ (π β (β€β₯βπ) β (π...(π + 1)) = ((π...π) βͺ {(π + 1)})) | ||
Theorem | fzpred 10069 | Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
β’ (π β (β€β₯βπ) β (π...π) = ({π} βͺ ((π + 1)...π))) | ||
Theorem | fzpreddisj 10070 | A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.) |
β’ (π β (β€β₯βπ) β ({π} β© ((π + 1)...π)) = β ) | ||
Theorem | elfzp1 10071 | 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 10072 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (π β β€ β ((π + 1)...π) β (π...π)) | ||
Theorem | fzelp1 10073 | 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 10074 | 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 10075 | Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.) |
β’ ((π β β β§ πΌ β (1...(π β 1))) β (πΌ + 1) β (1...π)) | ||
Theorem | fzpr 10076 | A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β β€ β (π...(π + 1)) = {π, (π + 1)}) | ||
Theorem | fztp 10077 | 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 10078 | 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 10079 | (π...(π + 1)) is the disjoint union of (π...π) with {(π + 1)}. (Contributed by Mario Carneiro, 7-Mar-2014.) |
β’ ((π...π) β© {(π + 1)}) = β | ||
Theorem | fzdifsuc 10080 | Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.) |
β’ (π β (β€β₯βπ) β (π...π) = ((π...(π + 1)) β {(π + 1)})) | ||
Theorem | fzprval 10081* | 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 10082* | 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 10083 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
β’ (((π β β€ β§ π β β€) β§ (π½ β β€ β§ πΎ β β€)) β (πΎ β ((π½ β π)...(π½ β π)) β (π½ β πΎ) β (π...π))) | ||
Theorem | fzrev2 10084 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
β’ (((π β β€ β§ π β β€) β§ (π½ β β€ β§ πΎ β β€)) β (πΎ β (π...π) β (π½ β πΎ) β ((π½ β π)...(π½ β π)))) | ||
Theorem | fzrev2i 10085 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
β’ ((π½ β β€ β§ πΎ β (π...π)) β (π½ β πΎ) β ((π½ β π)...(π½ β π))) | ||
Theorem | fzrev3 10086 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
β’ (πΎ β β€ β (πΎ β (π...π) β ((π + π) β πΎ) β (π...π))) | ||
Theorem | fzrev3i 10087 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
β’ (πΎ β (π...π) β ((π + π) β πΎ) β (π...π)) | ||
Theorem | fznn 10088 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
β’ (π β β€ β (πΎ β (1...π) β (πΎ β β β§ πΎ β€ π))) | ||
Theorem | elfz1b 10089 | Membership in a 1 based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) |
β’ (π β (1...π) β (π β β β§ π β β β§ π β€ π)) | ||
Theorem | elfzm11 10090 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (πΎ β (π...(π β 1)) β (πΎ β β€ β§ π β€ πΎ β§ πΎ < π))) | ||
Theorem | uzsplit 10091 | Express an upper integer set as the disjoint (see uzdisj 10092) union of the first π values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ (π β (β€β₯βπ) β (β€β₯βπ) = ((π...(π β 1)) βͺ (β€β₯βπ))) | ||
Theorem | uzdisj 10092 | The first π elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ ((π...(π β 1)) β© (β€β₯βπ)) = β | ||
Theorem | fseq1p1m1 10093 | 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 10094 | 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 10095* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
β’ (π β β€ β (βπ β (π...π)π β [π / π]π)) | ||
Theorem | elfzp1b 10096 | 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 10097 | 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 10098 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
β’ (π β (β€β₯βπ) β (πΎ β (π...π) β (πΎ = π β¨ πΎ β ((π + 1)...π)))) | ||
Theorem | fzm1 10099 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β (β€β₯βπ) β (πΎ β (π...π) β (πΎ β (π...(π β 1)) β¨ πΎ = π))) | ||
Theorem | fzneuz 10100 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
β’ ((π β (β€β₯βπ) β§ πΎ β β€) β Β¬ (π...π) = (β€β₯βπΎ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |