![]() |
Metamath
Proof Explorer Theorem List (p. 136 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elfzelz 13501 | A member of a finite set of sequential integers is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΎ β (π...π) β πΎ β β€) | ||
Theorem | elfzelzd 13502 | A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β πΎ β (π...π)) β β’ (π β πΎ β β€) | ||
Theorem | fzssz 13503 | A finite sequence of integers is a set of integers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π...π) β β€ | ||
Theorem | elfzle1 13504 | 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 13505 | 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 13506 | 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 13507 | 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 13508 | 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 13509 | 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 13510 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.) |
β’ (π β (β€β₯βπ) β π β (π...π)) | ||
Theorem | elfz3 13511 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.) |
β’ (π β β€ β π β (π...π)) | ||
Theorem | elfz1eq 13512 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.) |
β’ (πΎ β (π...π) β πΎ = π) | ||
Theorem | elfzubelfz 13513 | 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 13514 | A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.) |
β’ ((πΎ β (β€β₯βπ) β§ (πΎ + 1) β (π...π)) β πΎ β (π...π)) | ||
Theorem | fzn0 13515 | Properties of a finite interval of integers which is nonempty. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ ((π...π) β β β π β (β€β₯βπ)) | ||
Theorem | fz0 13516 | A finite set of sequential integers is empty if its bounds are not integers. (Contributed by AV, 13-Oct-2018.) |
β’ ((π β β€ β¨ π β β€) β (π...π) = β ) | ||
Theorem | fzn 13517 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.) |
β’ ((π β β€ β§ π β β€) β (π < π β (π...π) = β )) | ||
Theorem | fzen 13518 | A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.) |
β’ ((π β β€ β§ π β β€ β§ πΎ β β€) β (π...π) β ((π + πΎ)...(π + πΎ))) | ||
Theorem | fz1n 13519 | 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 | 0nelfz1 13520 | 0 is not an element of a finite interval of integers starting at 1. (Contributed by AV, 27-Aug-2020.) |
β’ 0 β (1...π) | ||
Theorem | 0fz1 13521 | Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.) |
β’ ((π β β0 β§ πΉ Fn (1...π)) β (πΉ = β β π = 0)) | ||
Theorem | fz10 13522 | 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 13523 | 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 13524 | 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 13525 | 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 13526 | Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
β’ (((πΎ + 1) β (β€β₯βπ) β§ π β (β€β₯βπΎ)) β (π...π) = ((π...πΎ) βͺ ((πΎ + 1)...π))) | ||
Theorem | fzsplit 13527 | 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 13528 | Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.) |
β’ (πΎ < π β ((π½...πΎ) β© (π...π)) = β ) | ||
Theorem | fz01en 13529 | 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.) |
β’ (π β β€ β (0...(π β 1)) β (1...π)) | ||
Theorem | elfznn 13530 | 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 13531 | A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (π΄ β β β π΄ β (1...π΄)) | ||
Theorem | fz1ssnn 13532 | A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ (1...π΄) β β | ||
Theorem | fznn0sub 13533 | 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 13534 | 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 13535 | Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
β’ (((π β β€ β§ π β β€) β§ (π½ β β€ β§ πΎ β β€)) β (π½ β (π...π) β (π½ + πΎ) β ((π + πΎ)...(π + πΎ)))) | ||
Theorem | fzadd2 13536 | Membership of a sum in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
β’ (((π β β€ β§ π β β€) β§ (π β β€ β§ π β β€)) β ((π½ β (π...π) β§ πΎ β (π...π)) β (π½ + πΎ) β ((π + π)...(π + π)))) | ||
Theorem | fzsubel 13537 | Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
β’ (((π β β€ β§ π β β€) β§ (π½ β β€ β§ πΎ β β€)) β (π½ β (π...π) β (π½ β πΎ) β ((π β πΎ)...(π β πΎ)))) | ||
Theorem | fzopth 13538 | A finite set of sequential integers has the ordered pair property (compare opth 5477) under certain conditions. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (π β (β€β₯βπ) β ((π...π) = (π½...πΎ) β (π = π½ β§ π = πΎ))) | ||
Theorem | fzass4 13539 | Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π΅ β (π΄...π·) β§ πΆ β (π΅...π·)) β (π΅ β (π΄...πΆ) β§ πΆ β (π΄...π·))) | ||
Theorem | fzss1 13540 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
β’ (πΎ β (β€β₯βπ) β (πΎ...π) β (π...π)) | ||
Theorem | fzss2 13541 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ (π β (β€β₯βπΎ) β (π...πΎ) β (π...π)) | ||
Theorem | fzssuz 13542 | A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
β’ (π...π) β (β€β₯βπ) | ||
Theorem | fzsn 13543 | A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β β€ β (π...π) = {π}) | ||
Theorem | fzssp1 13544 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (π...π) β (π...(π + 1)) | ||
Theorem | fzssnn 13545 | Finite sets of sequential integers starting from a natural are a subset of the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
β’ (π β β β (π...π) β β) | ||
Theorem | ssfzunsnext 13546 | A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 13-Nov-2021.) |
β’ ((π β (π...π) β§ (π β β€ β§ π β β€ β§ πΌ β β€)) β (π βͺ {πΌ}) β (if(πΌ β€ π, πΌ, π)...if(πΌ β€ π, π, πΌ))) | ||
Theorem | ssfzunsn 13547 | A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 8-Jun-2021.) (Proof shortened by AV, 13-Nov-2021.) |
β’ ((π β (π...π) β§ π β β€ β§ πΌ β (β€β₯βπ)) β (π βͺ {πΌ}) β (π...if(πΌ β€ π, π, πΌ))) | ||
Theorem | fzsuc 13548 | 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 13549 | Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
β’ (π β (β€β₯βπ) β (π...π) = ({π} βͺ ((π + 1)...π))) | ||
Theorem | fzpreddisj 13550 | A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.) |
β’ (π β (β€β₯βπ) β ({π} β© ((π + 1)...π)) = β ) | ||
Theorem | elfzp1 13551 | 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 13552 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (π β β€ β ((π + 1)...π) β (π...π)) | ||
Theorem | fzelp1 13553 | 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 13554 | 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 13555 | Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.) |
β’ ((π β β β§ πΌ β (1...(π β 1))) β (πΌ + 1) β (1...π)) | ||
Theorem | fzpr 13556 | A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β β€ β (π...(π + 1)) = {π, (π + 1)}) | ||
Theorem | fztp 13557 | 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 | fz12pr 13558 | An integer range between 1 and 2 is a pair. (Contributed by AV, 11-Jan-2023.) |
β’ (1...2) = {1, 2} | ||
Theorem | fzsuc2 13559 | 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 13560 | (π...(π + 1)) is the disjoint union of (π...π) with {(π + 1)}. (Contributed by Mario Carneiro, 7-Mar-2014.) |
β’ ((π...π) β© {(π + 1)}) = β | ||
Theorem | fzdifsuc 13561 | Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.) |
β’ (π β (β€β₯βπ) β (π...π) = ((π...(π + 1)) β {(π + 1)})) | ||
Theorem | fzprval 13562* | 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 13563* | 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 13564 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
β’ (((π β β€ β§ π β β€) β§ (π½ β β€ β§ πΎ β β€)) β (πΎ β ((π½ β π)...(π½ β π)) β (π½ β πΎ) β (π...π))) | ||
Theorem | fzrev2 13565 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
β’ (((π β β€ β§ π β β€) β§ (π½ β β€ β§ πΎ β β€)) β (πΎ β (π...π) β (π½ β πΎ) β ((π½ β π)...(π½ β π)))) | ||
Theorem | fzrev2i 13566 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
β’ ((π½ β β€ β§ πΎ β (π...π)) β (π½ β πΎ) β ((π½ β π)...(π½ β π))) | ||
Theorem | fzrev3 13567 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
β’ (πΎ β β€ β (πΎ β (π...π) β ((π + π) β πΎ) β (π...π))) | ||
Theorem | fzrev3i 13568 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
β’ (πΎ β (π...π) β ((π + π) β πΎ) β (π...π)) | ||
Theorem | fznn 13569 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
β’ (π β β€ β (πΎ β (1...π) β (πΎ β β β§ πΎ β€ π))) | ||
Theorem | elfz1b 13570 | Membership in a 1-based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) (Proof shortened by AV, 23-Jan-2022.) |
β’ (π β (1...π) β (π β β β§ π β β β§ π β€ π)) | ||
Theorem | elfz1uz 13571 | Membership in a 1-based finite set of sequential integers with an upper integer. (Contributed by AV, 23-Jan-2022.) |
β’ ((π β β β§ π β (β€β₯βπ)) β π β (1...π)) | ||
Theorem | elfzm11 13572 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (πΎ β (π...(π β 1)) β (πΎ β β€ β§ π β€ πΎ β§ πΎ < π))) | ||
Theorem | uzsplit 13573 | Express an upper integer set as the disjoint (see uzdisj 13574) union of the first π values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ (π β (β€β₯βπ) β (β€β₯βπ) = ((π...(π β 1)) βͺ (β€β₯βπ))) | ||
Theorem | uzdisj 13574 | The first π elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ ((π...(π β 1)) β© (β€β₯βπ)) = β | ||
Theorem | fseq1p1m1 13575 | 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 13576 | 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 13577* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
β’ (π β β€ β (βπ β (π...π)π β [π / π]π)) | ||
Theorem | elfzp1b 13578 | 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 13579 | 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 13580 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
β’ (π β (β€β₯βπ) β (πΎ β (π...π) β (πΎ = π β¨ πΎ β ((π + 1)...π)))) | ||
Theorem | fzm1 13581 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β (β€β₯βπ) β (πΎ β (π...π) β (πΎ β (π...(π β 1)) β¨ πΎ = π))) | ||
Theorem | fzneuz 13582 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
β’ ((π β (β€β₯βπ) β§ πΎ β β€) β Β¬ (π...π) = (β€β₯βπΎ)) | ||
Theorem | fznuz 13583 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 30-Jun-2013.) (Revised by Mario Carneiro, 24-Aug-2013.) |
β’ (πΎ β (π...π) β Β¬ πΎ β (β€β₯β(π + 1))) | ||
Theorem | uznfz 13584 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
β’ (πΎ β (β€β₯βπ) β Β¬ πΎ β (π...(π β 1))) | ||
Theorem | fzp1nel 13585 | 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.) |
β’ Β¬ (π + 1) β (π...π) | ||
Theorem | fzrevral 13586* | Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
β’ ((π β β€ β§ π β β€ β§ πΎ β β€) β (βπ β (π...π)π β βπ β ((πΎ β π)...(πΎ β π))[(πΎ β π) / π]π)) | ||
Theorem | fzrevral2 13587* | Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
β’ ((π β β€ β§ π β β€ β§ πΎ β β€) β (βπ β ((πΎ β π)...(πΎ β π))π β βπ β (π...π)[(πΎ β π) / π]π)) | ||
Theorem | fzrevral3 13588* | Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
β’ ((π β β€ β§ π β β€) β (βπ β (π...π)π β βπ β (π...π)[((π + π) β π) / π]π)) | ||
Theorem | fzshftral 13589* | Shift the scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
β’ ((π β β€ β§ π β β€ β§ πΎ β β€) β (βπ β (π...π)π β βπ β ((π + πΎ)...(π + πΎ))[(π β πΎ) / π]π)) | ||
Theorem | ige2m1fz1 13590 | 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.) |
β’ (π β (β€β₯β2) β (π β 1) β (1...π)) | ||
Theorem | ige2m1fz 13591 | 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.) |
β’ ((π β β0 β§ 2 β€ π) β (π β 1) β (0...π)) | ||
Finite intervals of nonnegative integers (or "finite sets of sequential nonnegative integers") are finite intervals of integers with 0 as lower bound: (0...π), usually abbreviated by "fz0". | ||
Theorem | elfz2nn0 13592 | Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΎ β (0...π) β (πΎ β β0 β§ π β β0 β§ πΎ β€ π)) | ||
Theorem | fznn0 13593 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
β’ (π β β0 β (πΎ β (0...π) β (πΎ β β0 β§ πΎ β€ π))) | ||
Theorem | elfznn0 13594 | 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.) |
β’ (πΎ β (0...π) β πΎ β β0) | ||
Theorem | elfz3nn0 13595 | 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.) |
β’ (πΎ β (0...π) β π β β0) | ||
Theorem | fz0ssnn0 13596 | Finite sets of sequential nonnegative integers starting with 0 are subsets of NN0. (Contributed by JJ, 1-Jun-2021.) |
β’ (0...π) β β0 | ||
Theorem | fz1ssfz0 13597 | Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (1...π) β (0...π) | ||
Theorem | 0elfz 13598 | 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.) |
β’ (π β β0 β 0 β (0...π)) | ||
Theorem | nn0fz0 13599 | 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.) |
β’ (π β β0 β π β (0...π)) | ||
Theorem | elfz0add 13600 | 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.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π β (0...π΄) β π β (0...(π΄ + π΅)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |