![]() |
Intuitionistic Logic Explorer Theorem List (p. 102 of 153) | < 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 | fztpval 10101* |
Two ways of defining the first three values of a sequence on ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzrev 10102 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzrev2 10103 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzrev2i 10104 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzrev3 10105 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzrev3i 10106 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fznn 10107 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfz1b 10108 | Membership in a 1 based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzm11 10109 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | uzsplit 10110 |
Express an upper integer set as the disjoint (see uzdisj 10111) union of
the first ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | uzdisj 10111 |
The first ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fseq1p1m1 10112 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fseq1m1p1 10113 | Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fz1sbc 10114* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzp1b 10115 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzm1b 10116 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzp12 10117 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzm1 10118 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzneuz 10119 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fznuz 10120 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 30-Jun-2013.) (Revised by Mario Carneiro, 24-Aug-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | uznfz 10121 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzp1nel 10122 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzrevral 10123* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzrevral2 10124* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzrevral3 10125* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzshftral 10126* | Shift the scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ige2m1fz1 10127 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | ige2m1fz 10128 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fz01or 10129 | An integer is in the integer range from zero to one iff it is either zero or one. (Contributed by Jim Kingdon, 11-Nov-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Finite intervals of nonnegative integers (or "finite sets of sequential
nonnegative integers") are finite intervals of integers with 0 as lower
bound:
| ||
Theorem | elfz2nn0 10130 | Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fznn0 10131 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfznn0 10132 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfz3nn0 10133 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fz0ssnn0 10134 | Finite sets of sequential nonnegative integers starting with 0 are subsets of NN0. (Contributed by JJ, 1-Jun-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fz1ssfz0 10135 | Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 0elfz 10136 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nn0fz0 10137 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfz0add 10138 | 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.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fz0sn 10139 | An integer range from 0 to 0 is a singleton. (Contributed by AV, 18-Apr-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fz0tp 10140 | An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fz0to3un2pr 10141 | An integer range from 0 to 3 is the union of two unordered pairs. (Contributed by AV, 7-Feb-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fz0to4untppr 10142 | An integer range from 0 to 4 is the union of a triple and a pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfz0ubfz0 10143 | An element of a finite set of sequential nonnegative integers is an element of a finite set of sequential nonnegative integers with the upper bound being an element of the finite set of sequential nonnegative integers with the same lower bound as for the first interval and the element under consideration as upper bound. (Contributed by Alexander van der Vekens, 3-Apr-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfz0fzfz0 10144 | A member of a finite set of sequential nonnegative integers is a member of a finite set of sequential nonnegative integers with a member of a finite set of sequential nonnegative integers starting at the upper bound of the first interval. (Contributed by Alexander van der Vekens, 27-May-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fz0fzelfz0 10145 | If a member of a finite set of sequential integers with a lower bound being a member of a finite set of sequential nonnegative integers with the same upper bound, this member is also a member of the finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 21-Apr-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fznn0sub2 10146 | Subtraction closure for a member of a finite set of sequential nonnegative integers. (Contributed by NM, 26-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | uzsubfz0 10147 | Membership of an integer greater than L decreased by L in a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 16-Sep-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fz0fzdiffz0 10148 | The difference of an integer in a finite set of sequential nonnegative integers and and an integer of a finite set of sequential integers with the same upper bound and the nonnegative integer as lower bound is a member of the finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 6-Jun-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzmlbm 10149 | Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzmlbp 10150 | Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzctr 10151 | Lemma for theorems about the central binomial coefficient. (Contributed by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 2-Aug-2014.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | difelfzle 10152 | The difference of two integers from a finite set of sequential nonnegative integers is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | difelfznle 10153 | The difference of two integers from a finite set of sequential nonnegative integers increased by the upper bound is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nn0split 10154 |
Express the set of nonnegative integers as the disjoint (see nn0disj 10156)
union of the first ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nnsplit 10155 |
Express the set of positive integers as the disjoint union of the first
![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | nn0disj 10156 |
The first ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1fv 10157 | A function on a singleton. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4fvwrd4 10158* | The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2ffzeq 10159* | Two functions over 0 based finite set of sequential integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | cfzo 10160 | Syntax for half-open integer ranges. |
![]() | ||
Definition | df-fzo 10161* |
Define a function generating sets of integers using a half-open range.
Read ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzof 10162 | Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzoel1 10163 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzoel2 10164 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzoelz 10165 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzoval 10166 | Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzo 10167 | Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzo2 10168 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzouz 10169 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzodcel 10170 | Decidability of membership in a half-open integer interval. (Contributed by Jim Kingdon, 25-Aug-2022.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzolb 10171 |
The left endpoint of a half-open integer interval is in the set iff the
two arguments are integers with ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzolb2 10172 |
The left endpoint of a half-open integer interval is in the set iff the
two arguments are integers with ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzole1 10173 | A member in a half-open integer interval is greater than or equal to the lower bound. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzolt2 10174 | A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzolt3 10175 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzolt2b 10176 | A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzolt3b 10177 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzonel 10178 | A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzouz2 10179 | The upper bound of a half-open range is greater or equal to an element of the range. (Contributed by Mario Carneiro, 29-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzofz 10180 | A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzo3 10181 |
Express membership in a half-open integer interval in terms of the "less
than or equal" and "less than" predicates on integers,
resp.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzom 10182* | A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzossfz 10183 | A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzon 10184 | A half-open set of sequential integers is empty if the bounds are equal or reversed. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzonlt0 10185 | A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzo0 10186 | Half-open sets with equal endpoints are empty. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzonnsub 10187 |
If ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzonnsub2 10188 |
If ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzoss1 10189 | Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzoss2 10190 | Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzossrbm1 10191 | Subset of a half open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzo0ss1 10192 | Subset relationship for half-open integer ranges with lower bounds 0 and 1. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzossnn0 10193 | A half-open integer range starting at a nonnegative integer is a subset of the nonnegative integers. (Contributed by Alexander van der Vekens, 13-May-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzospliti 10194 | One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzosplit 10195 | Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzodisj 10196 | Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzouzsplit 10197 | Split an upper integer set into a half-open integer range and another upper integer set. (Contributed by Mario Carneiro, 21-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | fzouzdisj 10198 | A half-open integer range does not overlap the upper integer range starting at the endpoint of the first range. (Contributed by Mario Carneiro, 21-Sep-2016.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | lbfzo0 10199 |
An integer is strictly greater than zero iff it is a member of ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | elfzo0 10200 | Membership in a half-open integer range based at 0. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |