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