P. 100 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9901-10000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fz0tp 9901	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	elfz0ubfz0 9902	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.)
|- ( ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) -> K e. ( 0 ... L ) )
Theorem	elfz0fzfz0 9903	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.)
|- ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> M e. ( 0 ... N ) )
Theorem	fz0fzelfz0 9904	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.)
|- ( ( N e. ( 0 ... R ) /\ M e. ( N ... R ) ) -> M e. ( 0 ... R ) )
Theorem	fznn0sub2 9905	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.)
|- ( K e. ( 0 ... N ) -> ( N - K ) e. ( 0 ... N ) )
Theorem	uzsubfz0 9906	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.)
|- ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> ( N - L ) e. ( 0 ... N ) )
Theorem	fz0fzdiffz0 9907	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.)
|- ( ( M e. ( 0 ... N ) /\ K e. ( M ... N ) ) -> ( K - M ) e. ( 0 ... N ) )
Theorem	elfzmlbm 9908	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.)
|- ( K e. ( M ... N ) -> ( K - M ) e. ( 0 ... ( N - M ) ) )
Theorem	elfzmlbp 9909	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.)
|- ( ( N e. ZZ /\ K e. ( M ... ( M + N ) ) ) -> ( K - M ) e. ( 0 ... N ) )
Theorem	fzctr 9910	Lemma for theorems about the central binomial coefficient. (Contributed by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 2-Aug-2014.)
|- ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
Theorem	difelfzle 9911	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.)
|- ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ K <_ M ) -> ( M - K ) e. ( 0 ... N ) )
Theorem	difelfznle 9912	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.)
|- ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) /\ -. K <_ M ) -> ( ( M + N ) - K ) e. ( 0 ... N ) )
Theorem	nn0split 9913	Express the set of nonnegative integers as the disjoint (see nn0disj 9915) union of the first N + 1 values and the rest. (Contributed by AV, 8-Nov-2019.)
|- ( N e. NN0 -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
Theorem	nnsplit 9914	Express the set of positive integers as the disjoint union of the first N values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( N e. NN -> NN = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
Theorem	nn0disj 9915	The first N + 1 elements of the set of nonnegative integers are distinct from any later members. (Contributed by AV, 8-Nov-2019.)
|- ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)
Theorem	1fv 9916	A function on a singleton. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
|- ( ( N e. V /\ P = { <. 0 , N >. } ) -> ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) )
Theorem	4fvwrd4 9917*	The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017.)
|- ( ( L e. ( ZZ>= ` 3 ) /\ P : ( 0 ... L ) --> V ) -> E. a e. V E. b e. V E. c e. V E. d e. V ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b ) /\ ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) )
Theorem	2ffzeq 9918*	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.)
|- ( ( M e. NN0 /\ F : ( 0 ... M ) --> X /\ P : ( 0 ... N ) --> Y ) -> ( F = P <-> ( M = N /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) ) )
4.5.6  Half-open integer ranges
Syntax	cfzo 9919	Syntax for half-open integer ranges.
class ..^
Definition	df-fzo 9920*	Define a function generating sets of integers using a half-open range. Read ( M..^ N ) as the integers from M up to, but not including, N; contrast with ( M ... N ) df-fz 9791, which includes N. Not including the endpoint simplifies a number of formulas related to cardinality and splitting; contrast fzosplit 9954 with fzsplit 9831, for instance. (Contributed by Stefan O'Rear, 14-Aug-2015.)
|- ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
Theorem	fzof 9921	Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015.)
|- ..^ : ( ZZ X. ZZ ) --> ~P ZZ
Theorem	elfzoel1 9922	Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)
|- ( A e. ( B..^ C ) -> B e. ZZ )
Theorem	elfzoel2 9923	Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)
|- ( A e. ( B..^ C ) -> C e. ZZ )
Theorem	elfzoelz 9924	Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)
|- ( A e. ( B..^ C ) -> A e. ZZ )
Theorem	fzoval 9925	Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015.)
|- ( N e. ZZ -> ( M..^ N ) = ( M ... ( N - 1 ) ) )
Theorem	elfzo 9926	Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M..^ N ) <-> ( M <_ K /\ K < N ) ) )
Theorem	elfzo2 9927	Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.)
|- ( K e. ( M..^ N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) )
Theorem	elfzouz 9928	Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.)
|- ( K e. ( M..^ N ) -> K e. ( ZZ>= ` M ) )
Theorem	fzodcel 9929	Decidability of membership in a half-open integer interval. (Contributed by Jim Kingdon, 25-Aug-2022.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> DECID K e. ( M..^ N ) )
Theorem	fzolb 9930	The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with M < N. This provides an alternate notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate M e. ( ZZ>= ` N ). (Contributed by Mario Carneiro, 29-Sep-2015.)
|- ( M e. ( M..^ N ) <-> ( M e. ZZ /\ N e. ZZ /\ M < N ) )
Theorem	fzolb2 9931	The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with M < N. This provides an alternate notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate M e. ( ZZ>= ` N ). (Contributed by Mario Carneiro, 29-Sep-2015.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. ( M..^ N ) <-> M < N ) )
Theorem	elfzole1 9932	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.)
|- ( K e. ( M..^ N ) -> M <_ K )
Theorem	elfzolt2 9933	A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( K e. ( M..^ N ) -> K < N )
Theorem	elfzolt3 9934	Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( K e. ( M..^ N ) -> M < N )
Theorem	elfzolt2b 9935	A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015.)
|- ( K e. ( M..^ N ) -> K e. ( K..^ N ) )
Theorem	elfzolt3b 9936	Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015.)
|- ( K e. ( M..^ N ) -> M e. ( M..^ N ) )
Theorem	fzonel 9937	A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015.)
|- -. B e. ( A..^ B )
Theorem	elfzouz2 9938	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.)
|- ( K e. ( M..^ N ) -> N e. ( ZZ>= ` K ) )
Theorem	elfzofz 9939	A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( K e. ( M..^ N ) -> K e. ( M ... N ) )
Theorem	elfzo3 9940	Express membership in a half-open integer interval in terms of the "less than or equal" and "less than" predicates on integers, resp. K e. ( ZZ>= ` M ) <-> M <_ K, K e. ( K..^ N ) <-> K < N. (Contributed by Mario Carneiro, 29-Sep-2015.)
|- ( K e. ( M..^ N ) <-> ( K e. ( ZZ>= ` M ) /\ K e. ( K..^ N ) ) )
Theorem	fzom 9941*	A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.)
|- ( E. x x e. ( M..^ N ) <-> M e. ( M..^ N ) )
Theorem	fzossfz 9942	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.)
|- ( A..^ B ) C_ ( A ... B )
Theorem	fzon 9943	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.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N <_ M <-> ( M..^ N ) = (/) ) )
Theorem	fzonlt0 9944	A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( -. M < N <-> ( M..^ N ) = (/) ) )
Theorem	fzo0 9945	Half-open sets with equal endpoints are empty. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
|- ( A..^ A ) = (/)
Theorem	fzonnsub 9946	If K < N then N - K is a positive integer. (Contributed by Mario Carneiro, 29-Sep-2015.) (Revised by Mario Carneiro, 1-Jan-2017.)
|- ( K e. ( M..^ N ) -> ( N - K ) e. NN )
Theorem	fzonnsub2 9947	If M < N then N - M is a positive integer. (Contributed by Mario Carneiro, 1-Jan-2017.)
|- ( K e. ( M..^ N ) -> ( N - M ) e. NN )
Theorem	fzoss1 9948	Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
|- ( K e. ( ZZ>= ` M ) -> ( K..^ N ) C_ ( M..^ N ) )
Theorem	fzoss2 9949	Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
|- ( N e. ( ZZ>= ` K ) -> ( M..^ K ) C_ ( M..^ N ) )
Theorem	fzossrbm1 9950	Subset of a half open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
|- ( N e. ZZ -> ( 0..^ ( N - 1 ) ) C_ ( 0..^ N ) )
Theorem	fzo0ss1 9951	Subset relationship for half-open integer ranges with lower bounds 0 and 1. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
|- ( 1..^ N ) C_ ( 0..^ N )
Theorem	fzossnn0 9952	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.)
|- ( M e. NN0 -> ( M..^ N ) C_ NN0 )
Theorem	fzospliti 9953	One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.)
|- ( ( A e. ( B..^ C ) /\ D e. ZZ ) -> ( A e. ( B..^ D ) \/ A e. ( D..^ C ) ) )
Theorem	fzosplit 9954	Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.)
|- ( D e. ( B ... C ) -> ( B..^ C ) = ( ( B..^ D ) u. ( D..^ C ) ) )
Theorem	fzodisj 9955	Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015.)
|- ( ( A..^ B ) i^i ( B..^ C ) ) = (/)
Theorem	fzouzsplit 9956	Split an upper integer set into a half-open integer range and another upper integer set. (Contributed by Mario Carneiro, 21-Sep-2016.)
|- ( B e. ( ZZ>= ` A ) -> ( ZZ>= ` A ) = ( ( A..^ B ) u. ( ZZ>= ` B ) ) )
Theorem	fzouzdisj 9957	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.)
|- ( ( A..^ B ) i^i ( ZZ>= ` B ) ) = (/)
Theorem	lbfzo0 9958	An integer is strictly greater than zero iff it is a member of NN. (Contributed by Mario Carneiro, 29-Sep-2015.)
|- ( 0 e. ( 0..^ A ) <-> A e. NN )
Theorem	elfzo0 9959	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.)
|- ( A e. ( 0..^ B ) <-> ( A e. NN0 /\ B e. NN /\ A < B ) )
Theorem	fzo1fzo0n0 9960	An integer between 1 and an upper bound of a half-open integer range is not 0 and between 0 and the upper bound of the half-open integer range. (Contributed by Alexander van der Vekens, 21-Mar-2018.)
|- ( K e. ( 1..^ N ) <-> ( K e. ( 0..^ N ) /\ K =/= 0 ) )
Theorem	elfzo0z 9961	Membership in a half-open range of nonnegative integers, generalization of elfzo0 9959 requiring the upper bound to be an integer only. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
|- ( A e. ( 0..^ B ) <-> ( A e. NN0 /\ B e. ZZ /\ A < B ) )
Theorem	elfzo0le 9962	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.)
|- ( A e. ( 0..^ B ) -> A <_ B )
Theorem	elfzonn0 9963	A member of a half-open range of nonnegative integers is a nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
|- ( K e. ( 0..^ N ) -> K e. NN0 )
Theorem	fzonmapblen 9964	The result of subtracting a nonnegative integer from a positive integer and adding another nonnegative integer which is less than the first one is less then the positive integer. (Contributed by Alexander van der Vekens, 19-May-2018.)
|- ( ( A e. ( 0..^ N ) /\ B e. ( 0..^ N ) /\ B < A ) -> ( B + ( N - A ) ) < N )
Theorem	fzofzim 9965	If a nonnegative integer in a finite interval of integers is not the upper bound of the interval, it is contained in the corresponding half-open integer range. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
|- ( ( K =/= M /\ K e. ( 0 ... M ) ) -> K e. ( 0..^ M ) )
Theorem	fzossnn 9966	Half-open integer ranges starting with 1 are subsets of NN. (Contributed by Thierry Arnoux, 28-Dec-2016.)
|- ( 1..^ N ) C_ NN
Theorem	elfzo1 9967	Membership in a half-open integer range based at 1. (Contributed by Thierry Arnoux, 14-Feb-2017.)
|- ( N e. ( 1..^ M ) <-> ( N e. NN /\ M e. NN /\ N < M ) )
Theorem	fzo0m 9968*	A half-open integer range based at 0 is inhabited precisely if the upper bound is a positive integer. (Contributed by Jim Kingdon, 20-Apr-2020.)
|- ( E. x x e. ( 0..^ A ) <-> A e. NN )
Theorem	fzoaddel 9969	Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( A e. ( B..^ C ) /\ D e. ZZ ) -> ( A + D ) e. ( ( B + D )..^ ( C + D ) ) )
Theorem	fzoaddel2 9970	Translate membership in a shifted-down half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( A e. ( 0..^ ( B - C ) ) /\ B e. ZZ /\ C e. ZZ ) -> ( A + C ) e. ( C..^ B ) )
Theorem	fzosubel 9971	Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( A e. ( B..^ C ) /\ D e. ZZ ) -> ( A - D ) e. ( ( B - D )..^ ( C - D ) ) )
Theorem	fzosubel2 9972	Membership in a translated half-open integer range implies translated membership in the original range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( A e. ( ( B + C )..^ ( B + D ) ) /\ ( B e. ZZ /\ C e. ZZ /\ D e. ZZ ) ) -> ( A - B ) e. ( C..^ D ) )
Theorem	fzosubel3 9973	Membership in a translated half-open integer range when the original range is zero-based. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( A e. ( B..^ ( B + D ) ) /\ D e. ZZ ) -> ( A - B ) e. ( 0..^ D ) )
Theorem	eluzgtdifelfzo 9974	Membership of the difference of integers in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( N e. ( ZZ>= ` A ) /\ B < A ) -> ( N - A ) e. ( 0..^ ( N - B ) ) ) )
Theorem	ige2m2fzo 9975	Membership of an integer greater than 1 decreased by 2 in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
|- ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. ( 0..^ ( N - 1 ) ) )
Theorem	fzocatel 9976	Translate membership in a half-open integer range. (Contributed by Thierry Arnoux, 28-Sep-2018.)
|- ( ( ( A e. ( 0..^ ( B + C ) ) /\ -. A e. ( 0..^ B ) ) /\ ( B e. ZZ /\ C e. ZZ ) ) -> ( A - B ) e. ( 0..^ C ) )
Theorem	ubmelfzo 9977	If an integer in a 1 based finite set of sequential integers is subtracted from the upper bound of this finite set of sequential integers, the result is contained in a half-open range of nonnegative integers with the same upper bound. (Contributed by AV, 18-Mar-2018.) (Revised by AV, 30-Oct-2018.)
|- ( K e. ( 1 ... N ) -> ( N - K ) e. ( 0..^ N ) )
Theorem	elfzodifsumelfzo 9978	If an integer is in a half-open range of nonnegative integers with a difference as upper bound, the sum of the integer with the subtrahend of the difference is in the a half-open range of nonnegative integers containing the minuend of the difference. (Contributed by AV, 13-Nov-2018.)
|- ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... P ) ) -> ( I e. ( 0..^ ( N - M ) ) -> ( I + M ) e. ( 0..^ P ) ) )
Theorem	elfzom1elp1fzo 9979	Membership of an integer incremented by one in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Proof shortened by AV, 5-Jan-2020.)
|- ( ( N e. ZZ /\ I e. ( 0..^ ( N - 1 ) ) ) -> ( I + 1 ) e. ( 0..^ N ) )
Theorem	elfzom1elfzo 9980	Membership in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 18-Jun-2018.)
|- ( ( N e. ZZ /\ I e. ( 0..^ ( N - 1 ) ) ) -> I e. ( 0..^ N ) )
Theorem	fzval3 9981	Expressing a closed integer range as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( N e. ZZ -> ( M ... N ) = ( M..^ ( N + 1 ) ) )
Theorem	fzosn 9982	Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( A e. ZZ -> ( A..^ ( A + 1 ) ) = { A } )
Theorem	elfzomin 9983	Membership of an integer in the smallest open range of integers. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( Z e. ZZ -> Z e. ( Z..^ ( Z + 1 ) ) )
Theorem	zpnn0elfzo 9984	Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( Z e. ZZ /\ N e. NN0 ) -> ( Z + N ) e. ( Z..^ ( ( Z + N ) + 1 ) ) )
Theorem	zpnn0elfzo1 9985	Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( Z e. ZZ /\ N e. NN0 ) -> ( Z + N ) e. ( Z..^ ( Z + ( N + 1 ) ) ) )
Theorem	fzosplitsnm1 9986	Removing a singleton from a half-open integer range at the end. (Contributed by Alexander van der Vekens, 23-Mar-2018.)
|- ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( A..^ B ) = ( ( A..^ ( B - 1 ) ) u. { ( B - 1 ) } ) )
Theorem	elfzonlteqm1 9987	If an element of a half-open integer range is not less than the upper bound of the range decreased by 1, it must be equal to the upper bound of the range decreased by 1. (Contributed by AV, 3-Nov-2018.)
|- ( ( A e. ( 0..^ B ) /\ -. A < ( B - 1 ) ) -> A = ( B - 1 ) )
Theorem	fzonn0p1 9988	A nonnegative integer is element of the half-open range of nonnegative integers with the element increased by one as an upper bound. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
|- ( N e. NN0 -> N e. ( 0..^ ( N + 1 ) ) )
Theorem	fzossfzop1 9989	A half-open range of nonnegative integers is a subset of a half-open range of nonnegative integers with the upper bound increased by one. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
|- ( N e. NN0 -> ( 0..^ N ) C_ ( 0..^ ( N + 1 ) ) )
Theorem	fzonn0p1p1 9990	If a nonnegative integer is element of a half-open range of nonnegative integers, increasing this integer by one results in an element of a half- open range of nonnegative integers with the upper bound increased by one. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
|- ( I e. ( 0..^ N ) -> ( I + 1 ) e. ( 0..^ ( N + 1 ) ) )
Theorem	elfzom1p1elfzo 9991	Increasing an element of a half-open range of nonnegative integers by 1 results in an element of the half-open range of nonnegative integers with an upper bound increased by 1. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
|- ( ( N e. NN /\ X e. ( 0..^ ( N - 1 ) ) ) -> ( X + 1 ) e. ( 0..^ N ) )
Theorem	fzo0ssnn0 9992	Half-open integer ranges starting with 0 are subsets of NN0. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- ( 0..^ N ) C_ NN0
Theorem	fzo01 9993	Expressing the singleton of 0 as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( 0..^ 1 ) = { 0 }
Theorem	fzo12sn 9994	A 1-based half-open integer interval up to, but not including, 2 is a singleton. (Contributed by Alexander van der Vekens, 31-Jan-2018.)
|- ( 1..^ 2 ) = { 1 }
Theorem	fzo0to2pr 9995	A half-open integer range from 0 to 2 is an unordered pair. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
|- ( 0..^ 2 ) = { 0 , 1 }
Theorem	fzo0to3tp 9996	A half-open integer range from 0 to 3 is an unordered triple. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
|- ( 0..^ 3 ) = { 0 , 1 , 2 }
Theorem	fzo0to42pr 9997	A half-open integer range from 0 to 4 is a union of two unordered pairs. (Contributed by Alexander van der Vekens, 17-Nov-2017.)
|- ( 0..^ 4 ) = ( { 0 , 1 } u. { 2 , 3 } )
Theorem	fzo0sn0fzo1 9998	A half-open range of nonnegative integers is the union of the singleton set containing 0 and a half-open range of positive integers. (Contributed by Alexander van der Vekens, 18-May-2018.)
|- ( N e. NN -> ( 0..^ N ) = ( { 0 } u. ( 1..^ N ) ) )
Theorem	fzoend 9999	The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015.)
|- ( A e. ( A..^ B ) -> ( B - 1 ) e. ( A..^ B ) )
Theorem	fzo0end 10000	The endpoint of a zero-based half-open range. (Contributed by Stefan O'Rear, 27-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
|- ( B e. NN -> ( B - 1 ) e. ( 0..^ B ) )