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