Home | Metamath
Proof Explorer Theorem List (p. 125 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fzprval 12401* | Two ways of defining the first two values of a sequence on . (Contributed by NM, 5-Sep-2011.) |
Theorem | fztpval 12402* | Two ways of defining the first three values of a sequence on . (Contributed by NM, 13-Sep-2011.) |
Theorem | fzrev 12403 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev2 12404 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev2i 12405 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrev3 12406 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fzrev3i 12407 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fznn 12408 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
Theorem | elfz1b 12409 | Membership in a 1 based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) (Proof shortened by AV, 23-Jan-2022.) |
Theorem | elfz1uz 12410 | Membership in a 1 based finite set of sequential integers with an upper integer. (Contributed by AV, 23-Jan-2022.) |
Theorem | elfzm11 12411 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | uzsplit 12412 | Express an upper integer set as the disjoint (see uzdisj 12413) union of the first values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
Theorem | uzdisj 12413 | The first elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
Theorem | fseq1p1m1 12414 | 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 12415 | Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | fz1sbc 12416* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
Theorem | elfzp1b 12417 | 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 12418 | 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 12419 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
Theorem | fzm1 12420 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fzneuz 12421 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
Theorem | fznuz 12422 | 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 12423 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
Theorem | fzp1nel 12424 | 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 12425* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrevral2 12426* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
Theorem | fzrevral3 12427* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
Theorem | fzshftral 12428* | Shift the scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
Theorem | ige2m1fz1 12429 | 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 12430 | 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.) |
Finite intervals of nonnegative integers (or "finite sets of sequential nonnegative integers") are finite intervals of integers with 0 as lower bound: , usually abbreviated by "fz0". | ||
Theorem | elfz2nn0 12431 | Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | fznn0 12432 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
Theorem | elfznn0 12433 | 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 12434 | 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 12435 | Finite sets of sequential nonnegative integers starting with 0 are subsets of NN0. (Contributed by JJ, 1-Jun-2021.) |
Theorem | 0elfz 12436 | 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 12437 | 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 12438 | 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 12439 | An integer range from 0 to 0 is a singleton. (Contributed by AV, 18-Apr-2021.) |
Theorem | fz0tp 12440 | An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
Theorem | fz0to3un2pr 12441 | An integer range from 0 to 3 is the union of two unordered pairs. (Contributed by AV, 7-Feb-2021.) |
Theorem | fz0to4untppr 12442 | 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 12443 | 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 12444 | 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 12445 | 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 12446 | 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 12447 | 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 12448 | 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 12449 | 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 12450 | 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 12451 | Lemma for theorems about the central binomial coefficient. (Contributed by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 2-Aug-2014.) |
Theorem | difelfzle 12452 | 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 12453 | 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 12454 | Express the set of nonnegative integers as the disjoint (see nn0disj 12455) union of the first values and the rest. (Contributed by AV, 8-Nov-2019.) |
Theorem | nn0disj 12455 | The first elements of the set of nonnegative integers are distinct from any later members. (Contributed by AV, 8-Nov-2019.) |
Theorem | fz0sn0fz1 12456 | A finite set of sequential nonnegative integers is the union of the singleton containing 0 and a finite set of sequential positive integers. (Contributed by AV, 20-Mar-2021.) |
Theorem | fvffz0 12457 | The function value of a function from a finite interval of nonnegative integers. (Contributed by AV, 13-Feb-2021.) |
Theorem | 1fv 12458 | A one value function. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Proof shortened by AV, 18-Apr-2021.) |
Theorem | 4fvwrd4 12459* | The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |
Theorem | 2ffzeq 12460* | 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.) |
Theorem | preduz 12461 | The value of the predecessor class over an upper integer set. (Contributed by Scott Fenton, 16-May-2014.) |
Theorem | prednn 12462 | The value of the predecessor class over the naturals. (Contributed by Scott Fenton, 6-Aug-2013.) |
Theorem | prednn0 12463 | The value of the predecessor class over . (Contributed by Scott Fenton, 9-May-2014.) |
Theorem | predfz 12464 | Calculate the predecessor of an integer under a finite set of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
Syntax | cfzo 12465 | Syntax for half-open integer ranges. |
..^ | ||
Definition | df-fzo 12466* | Define a function generating sets of integers using a half-open range. Read ..^ as the integers from up to, but not including, ; contrast with df-fz 12327, which includes . Not including the endpoint simplifies a number of formulae related to cardinality and splitting; contrast fzosplit 12501 with fzsplit 12367, for instance. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | fzof 12467 | Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | elfzoel1 12468 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | elfzoel2 12469 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | elfzoelz 12470 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | fzoval 12471 | Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ | ||
Theorem | elfzo 12472 | Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
..^ | ||
Theorem | elfzo2 12473 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ | ||
Theorem | elfzouz 12474 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ | ||
Theorem | nelfzo 12475 | An integer not being a member of a half-open finite set of integers. (Contributed by AV, 29-Apr-2020.) |
..^ | ||
Theorem | fzolb 12476 | The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with . This provides an alternative notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate . (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ | ||
Theorem | fzolb2 12477 | The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with . This provides an alternative notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate . (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ | ||
Theorem | elfzole1 12478 | 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 12479 | A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
..^ | ||
Theorem | elfzolt3 12480 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
..^ | ||
Theorem | elfzolt2b 12481 | A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ ..^ | ||
Theorem | elfzolt3b 12482 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ ..^ | ||
Theorem | fzonel 12483 | A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
..^ | ||
Theorem | elfzouz2 12484 | 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 12485 | A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
..^ | ||
Theorem | elfzo3 12486 | Express membership in a half-open integer interval in terms of the "less than or equal" and "less than" predicates on integers, resp. , ..^ . (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ ..^ | ||
Theorem | fzon0 12487 | A half-open integer interval is nonempty iff it contains its left endpoint. (Contributed by Mario Carneiro, 29-Sep-2015.) |
..^ ..^ | ||
Theorem | fzossfz 12488 | 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 12489 | 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 | fzo0n 12490 | A half-open range of nonnegative integers is empty iff the upper bound is not positive. (Contributed by AV, 2-May-2020.) |
..^ | ||
Theorem | fzonlt0 12491 | A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018.) |
..^ | ||
Theorem | fzo0 12492 | 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 12493 | If then is a positive integer. (Contributed by Mario Carneiro, 29-Sep-2015.) (Revised by Mario Carneiro, 1-Jan-2017.) |
..^ | ||
Theorem | fzonnsub2 12494 | If then is a positive integer. (Contributed by Mario Carneiro, 1-Jan-2017.) |
..^ | ||
Theorem | fzoss1 12495 | 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 12496 | 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 12497 | Subset of a half open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
..^ ..^ | ||
Theorem | fzo0ss1 12498 | Subset relationship for half-open integer ranges with lower bounds 0 and 1. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
..^ ..^ | ||
Theorem | fzossnn0 12499 | 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 12500 | One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ ..^ ..^ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |