![]() |
Metamath
Proof Explorer Theorem List (p. 137 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fz1sbc 13601* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
β’ (π β β€ β (βπ β (π...π)π β [π / π]π)) | ||
Theorem | elfzp1b 13602 | 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 13603 | 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 13604 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
β’ (π β (β€β₯βπ) β (πΎ β (π...π) β (πΎ = π β¨ πΎ β ((π + 1)...π)))) | ||
Theorem | fzm1 13605 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β (β€β₯βπ) β (πΎ β (π...π) β (πΎ β (π...(π β 1)) β¨ πΎ = π))) | ||
Theorem | fzneuz 13606 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
β’ ((π β (β€β₯βπ) β§ πΎ β β€) β Β¬ (π...π) = (β€β₯βπΎ)) | ||
Theorem | fznuz 13607 | 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 13608 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
β’ (πΎ β (β€β₯βπ) β Β¬ πΎ β (π...(π β 1))) | ||
Theorem | fzp1nel 13609 | 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 13610* | 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 13611* | 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 13612* | 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 13613* | 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 13614 | 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 13615 | 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 13616 | 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 13617 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
β’ (π β β0 β (πΎ β (0...π) β (πΎ β β0 β§ πΎ β€ π))) | ||
Theorem | elfznn0 13618 | 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 13619 | 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 13620 | Finite sets of sequential nonnegative integers starting with 0 are subsets of NN0. (Contributed by JJ, 1-Jun-2021.) |
β’ (0...π) β β0 | ||
Theorem | fz1ssfz0 13621 | Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (1...π) β (0...π) | ||
Theorem | 0elfz 13622 | 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 13623 | 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 13624 | 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...(π΄ + π΅)))) | ||
Theorem | fz0sn 13625 | An integer range from 0 to 0 is a singleton. (Contributed by AV, 18-Apr-2021.) |
β’ (0...0) = {0} | ||
Theorem | fz0tp 13626 | An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
β’ (0...2) = {0, 1, 2} | ||
Theorem | fz0to3un2pr 13627 | An integer range from 0 to 3 is the union of two unordered pairs. (Contributed by AV, 7-Feb-2021.) |
β’ (0...3) = ({0, 1} βͺ {2, 3}) | ||
Theorem | fz0to4untppr 13628 | 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.) |
β’ (0...4) = ({0, 1, 2} βͺ {3, 4}) | ||
Theorem | elfz0ubfz0 13629 | 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.) |
β’ ((πΎ β (0...π) β§ πΏ β (πΎ...π)) β πΎ β (0...πΏ)) | ||
Theorem | elfz0fzfz0 13630 | 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.) |
β’ ((π β (0...πΏ) β§ π β (πΏ...π)) β π β (0...π)) | ||
Theorem | fz0fzelfz0 13631 | 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.) |
β’ ((π β (0...π ) β§ π β (π...π )) β π β (0...π )) | ||
Theorem | fznn0sub2 13632 | 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.) |
β’ (πΎ β (0...π) β (π β πΎ) β (0...π)) | ||
Theorem | uzsubfz0 13633 | 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.) |
β’ ((πΏ β β0 β§ π β (β€β₯βπΏ)) β (π β πΏ) β (0...π)) | ||
Theorem | fz0fzdiffz0 13634 | 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.) |
β’ ((π β (0...π) β§ πΎ β (π...π)) β (πΎ β π) β (0...π)) | ||
Theorem | elfzmlbm 13635 | 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.) |
β’ (πΎ β (π...π) β (πΎ β π) β (0...(π β π))) | ||
Theorem | elfzmlbp 13636 | 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.) |
β’ ((π β β€ β§ πΎ β (π...(π + π))) β (πΎ β π) β (0...π)) | ||
Theorem | fzctr 13637 | Lemma for theorems about the central binomial coefficient. (Contributed by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 2-Aug-2014.) |
β’ (π β β0 β π β (0...(2 Β· π))) | ||
Theorem | difelfzle 13638 | 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.) |
β’ ((πΎ β (0...π) β§ π β (0...π) β§ πΎ β€ π) β (π β πΎ) β (0...π)) | ||
Theorem | difelfznle 13639 | 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.) |
β’ ((πΎ β (0...π) β§ π β (0...π) β§ Β¬ πΎ β€ π) β ((π + π) β πΎ) β (0...π)) | ||
Theorem | nn0split 13640 | Express the set of nonnegative integers as the disjoint (see nn0disj 13641) union of the first π + 1 values and the rest. (Contributed by AV, 8-Nov-2019.) |
β’ (π β β0 β β0 = ((0...π) βͺ (β€β₯β(π + 1)))) | ||
Theorem | nn0disj 13641 | The first π + 1 elements of the set of nonnegative integers are distinct from any later members. (Contributed by AV, 8-Nov-2019.) |
β’ ((0...π) β© (β€β₯β(π + 1))) = β | ||
Theorem | fz0sn0fz1 13642 | 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.) |
β’ (π β β0 β (0...π) = ({0} βͺ (1...π))) | ||
Theorem | fvffz0 13643 | The function value of a function from a finite interval of nonnegative integers. (Contributed by AV, 13-Feb-2021.) |
β’ (((π β β0 β§ πΌ β β0 β§ πΌ < π) β§ π:(0...π)βΆπ) β (πβπΌ) β π) | ||
Theorem | 1fv 13644 | A function on a singleton. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Proof shortened by AV, 18-Apr-2021.) |
β’ ((π β π β§ π = {β¨0, πβ©}) β (π:(0...0)βΆπ β§ (πβ0) = π)) | ||
Theorem | 4fvwrd4 13645* | The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |
β’ ((πΏ β (β€β₯β3) β§ π:(0...πΏ)βΆπ) β βπ β π βπ β π βπ β π βπ β π (((πβ0) = π β§ (πβ1) = π) β§ ((πβ2) = π β§ (πβ3) = π))) | ||
Theorem | 2ffzeq 13646* | 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.) |
β’ ((π β β0 β§ πΉ:(0...π)βΆπ β§ π:(0...π)βΆπ) β (πΉ = π β (π = π β§ βπ β (0...π)(πΉβπ) = (πβπ)))) | ||
Theorem | preduz 13647 | The value of the predecessor class over an upper integer set. (Contributed by Scott Fenton, 16-May-2014.) |
β’ (π β (β€β₯βπ) β Pred( < , (β€β₯βπ), π) = (π...(π β 1))) | ||
Theorem | prednn 13648 | The value of the predecessor class over the naturals. (Contributed by Scott Fenton, 6-Aug-2013.) |
β’ (π β β β Pred( < , β, π) = (1...(π β 1))) | ||
Theorem | prednn0 13649 | The value of the predecessor class over β0. (Contributed by Scott Fenton, 9-May-2014.) |
β’ (π β β0 β Pred( < , β0, π) = (0...(π β 1))) | ||
Theorem | predfz 13650 | 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.) |
β’ (πΎ β (π...π) β Pred( < , (π...π), πΎ) = (π...(πΎ β 1))) | ||
Syntax | cfzo 13651 | Syntax for half-open integer ranges. |
class ..^ | ||
Definition | df-fzo 13652* | 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 13509, which includes π. Not including the endpoint simplifies a number of formulas related to cardinality and splitting; contrast fzosplit 13689 with fzsplit 13551, for instance. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
β’ ..^ = (π β β€, π β β€ β¦ (π...(π β 1))) | ||
Theorem | fzof 13653 | Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
β’ ..^:(β€ Γ β€)βΆπ« β€ | ||
Theorem | elfzoel1 13654 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
β’ (π΄ β (π΅..^πΆ) β π΅ β β€) | ||
Theorem | elfzoel2 13655 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
β’ (π΄ β (π΅..^πΆ) β πΆ β β€) | ||
Theorem | elfzoelz 13656 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
β’ (π΄ β (π΅..^πΆ) β π΄ β β€) | ||
Theorem | fzoval 13657 | Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
β’ (π β β€ β (π..^π) = (π...(π β 1))) | ||
Theorem | elfzo 13658 | Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (πΎ β (π..^π) β (π β€ πΎ β§ πΎ < π))) | ||
Theorem | elfzo2 13659 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
β’ (πΎ β (π..^π) β (πΎ β (β€β₯βπ) β§ π β β€ β§ πΎ < π)) | ||
Theorem | elfzouz 13660 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
β’ (πΎ β (π..^π) β πΎ β (β€β₯βπ)) | ||
Theorem | nelfzo 13661 | An integer not being a member of a half-open finite set of integers. (Contributed by AV, 29-Apr-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (πΎ β (π..^π) β (πΎ < π β¨ π β€ πΎ))) | ||
Theorem | fzolb 13662 | 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 13663 | 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 13664 | 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 13665 | A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ (πΎ β (π..^π) β πΎ < π) | ||
Theorem | elfzolt3 13666 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ (πΎ β (π..^π) β π < π) | ||
Theorem | elfzolt2b 13667 | A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015.) |
β’ (πΎ β (π..^π) β πΎ β (πΎ..^π)) | ||
Theorem | elfzolt3b 13668 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015.) |
β’ (πΎ β (π..^π) β π β (π..^π)) | ||
Theorem | elfzop1le2 13669 | A member in a half-open integer interval plus 1 is less than or equal to the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (πΎ β (π..^π) β (πΎ + 1) β€ π) | ||
Theorem | fzonel 13670 | A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
β’ Β¬ π΅ β (π΄..^π΅) | ||
Theorem | elfzouz2 13671 | The upper bound of a half-open range is greater than or equal to an element of the range. (Contributed by Mario Carneiro, 29-Sep-2015.) |
β’ (πΎ β (π..^π) β π β (β€β₯βπΎ)) | ||
Theorem | elfzofz 13672 | A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ (πΎ β (π..^π) β πΎ β (π...π)) | ||
Theorem | elfzo3 13673 | Express membership in a half-open integer interval in terms of the "less than or equal to" and "less than" predicates on integers, resp. πΎ β (β€β₯βπ) β π β€ πΎ, πΎ β (πΎ..^π) β πΎ < π. (Contributed by Mario Carneiro, 29-Sep-2015.) |
β’ (πΎ β (π..^π) β (πΎ β (β€β₯βπ) β§ πΎ β (πΎ..^π))) | ||
Theorem | fzon0 13674 | A half-open integer interval is nonempty iff it contains its left endpoint. (Contributed by Mario Carneiro, 29-Sep-2015.) |
β’ ((π..^π) β β β π β (π..^π)) | ||
Theorem | fzossfz 13675 | 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 | fzossz 13676 | A half-open integer interval is a set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π..^π) β β€ | ||
Theorem | fzon 13677 | 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 13678 | A half-open range of nonnegative integers is empty iff the upper bound is not positive. (Contributed by AV, 2-May-2020.) |
β’ ((π β β€ β§ π β β€) β (π β€ π β (0..^(π β π)) = β )) | ||
Theorem | fzonlt0 13679 | A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018.) |
β’ ((π β β€ β§ π β β€) β (Β¬ π < π β (π..^π) = β )) | ||
Theorem | fzo0 13680 | 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 13681 | If πΎ < π then π β πΎ is a positive integer. (Contributed by Mario Carneiro, 29-Sep-2015.) (Revised by Mario Carneiro, 1-Jan-2017.) |
β’ (πΎ β (π..^π) β (π β πΎ) β β) | ||
Theorem | fzonnsub2 13682 | If π < π then π β π is a positive integer. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ (πΎ β (π..^π) β (π β π) β β) | ||
Theorem | fzoss1 13683 | 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 13684 | 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 13685 | Subset of a half-open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
β’ (π β β€ β (0..^(π β 1)) β (0..^π)) | ||
Theorem | fzo0ss1 13686 | Subset relationship for half-open integer ranges with lower bounds 0 and 1. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
β’ (1..^π) β (0..^π) | ||
Theorem | fzossnn0 13687 | 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.) |
β’ (π β β0 β (π..^π) β β0) | ||
Theorem | fzospliti 13688 | One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
β’ ((π΄ β (π΅..^πΆ) β§ π· β β€) β (π΄ β (π΅..^π·) β¨ π΄ β (π·..^πΆ))) | ||
Theorem | fzosplit 13689 | Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
β’ (π· β (π΅...πΆ) β (π΅..^πΆ) = ((π΅..^π·) βͺ (π·..^πΆ))) | ||
Theorem | fzodisj 13690 | Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
β’ ((π΄..^π΅) β© (π΅..^πΆ)) = β | ||
Theorem | fzouzsplit 13691 | 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 13692 | 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 | fzoun 13693 | A half-open integer range as union of two half-open integer ranges. (Contributed by AV, 23-Apr-2022.) |
β’ ((π΅ β (β€β₯βπ΄) β§ πΆ β β0) β (π΄..^(π΅ + πΆ)) = ((π΄..^π΅) βͺ (π΅..^(π΅ + πΆ)))) | ||
Theorem | fzodisjsn 13694 | A half-open integer range and the singleton of its upper bound are disjoint. (Contributed by AV, 7-Mar-2021.) |
β’ ((π΄..^π΅) β© {π΅}) = β | ||
Theorem | prinfzo0 13695 | The intersection of a half-open integer range and the pair of its outer left borders is empty. (Contributed by AV, 9-Jan-2021.) |
β’ (π β β€ β ({π, π} β© ((π + 1)..^π)) = β ) | ||
Theorem | lbfzo0 13696 | An integer is strictly greater than zero iff it is a member of β. (Contributed by Mario Carneiro, 29-Sep-2015.) |
β’ (0 β (0..^π΄) β π΄ β β) | ||
Theorem | elfzo0 13697 | 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.) |
β’ (π΄ β (0..^π΅) β (π΄ β β0 β§ π΅ β β β§ π΄ < π΅)) | ||
Theorem | elfzo0z 13698 | Membership in a half-open range of nonnegative integers, generalization of elfzo0 13697 requiring the upper bound to be an integer only. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
β’ (π΄ β (0..^π΅) β (π΄ β β0 β§ π΅ β β€ β§ π΄ < π΅)) | ||
Theorem | nn0p1elfzo 13699 | A nonnegative integer increased by 1 which is less than or equal to another integer is an element of a half-open range of integers. (Contributed by AV, 27-Feb-2021.) |
β’ ((πΎ β β0 β§ π β β0 β§ (πΎ + 1) β€ π) β πΎ β (0..^π)) | ||
Theorem | elfzo0le 13700 | A member in a half-open range of nonnegative integers is less than or equal to the upper bound of the range. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
β’ (π΄ β (0..^π΅) β π΄ β€ π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |