P. 105 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10401-10500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iooneg 10401	Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( A (,) B ) <-> -u C e. ( -u B (,) -u A ) ) )
Theorem	iccneg 10402	Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( A [,] B ) <-> -u C e. ( -u B [,] -u A ) ) )
Theorem	icoshft 10403	A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( X e. ( A [,) B ) -> ( X + C ) e. ( ( A + C ) [,) ( B + C ) ) ) )
Theorem	icoshftf1o 10404*	Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
|- F = ( x e. ( A [,) B ) |-> ( x + C ) )   =>    |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> F : ( A [,) B ) -1-1-onto-> ( ( A + C ) [,) ( B + C ) ) )
Theorem	icodisj 10405	End-to-end closed-below, open-above real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A [,) B ) i^i ( B [,) C ) ) = (/) )
Theorem	ioodisj 10406	If the upper bound of one open interval is less than or equal to the lower bound of the other, the intervals are disjoint. (Contributed by Jeff Hankins, 13-Jul-2009.)
|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) /\ B <_ C ) -> ( ( A (,) B ) i^i ( C (,) D ) ) = (/) )
Theorem	iccshftr 10407	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A + R ) = C   &    |- ( B + R ) = D   =>    |- ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ R e. RR ) ) -> ( X e. ( A [,] B ) <-> ( X + R ) e. ( C [,] D ) ) )
Theorem	iccshftri 10408	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- A e. RR   &    |- B e. RR   &    |- R e. RR   &    |- ( A + R ) = C   &    |- ( B + R ) = D   =>    |- ( X e. ( A [,] B ) -> ( X + R ) e. ( C [,] D ) )
Theorem	iccshftl 10409	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A - R ) = C   &    |- ( B - R ) = D   =>    |- ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ R e. RR ) ) -> ( X e. ( A [,] B ) <-> ( X - R ) e. ( C [,] D ) ) )
Theorem	iccshftli 10410	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- A e. RR   &    |- B e. RR   &    |- R e. RR   &    |- ( A - R ) = C   &    |- ( B - R ) = D   =>    |- ( X e. ( A [,] B ) -> ( X - R ) e. ( C [,] D ) )
Theorem	iccdil 10411	Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A x. R ) = C   &    |- ( B x. R ) = D   =>    |- ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ R e. RR+ ) ) -> ( X e. ( A [,] B ) <-> ( X x. R ) e. ( C [,] D ) ) )
Theorem	iccdili 10412	Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- A e. RR   &    |- B e. RR   &    |- R e. RR+   &    |- ( A x. R ) = C   &    |- ( B x. R ) = D   =>    |- ( X e. ( A [,] B ) -> ( X x. R ) e. ( C [,] D ) )
Theorem	icccntr 10413	Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A / R ) = C   &    |- ( B / R ) = D   =>    |- ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ R e. RR+ ) ) -> ( X e. ( A [,] B ) <-> ( X / R ) e. ( C [,] D ) ) )
Theorem	icccntri 10414	Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- A e. RR   &    |- B e. RR   &    |- R e. RR+   &    |- ( A / R ) = C   &    |- ( B / R ) = D   =>    |- ( X e. ( A [,] B ) -> ( X / R ) e. ( C [,] D ) )
Theorem	divelunit 10415	A condition for a ratio to be a member of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) e. ( 0 [,] 1 ) <-> A <_ B ) )
Theorem	lincmb01cmp 10416	A linear combination of two reals which lies in the interval between them. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 8-Sep-2015.)
|- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) x. A ) + ( T x. B ) ) e. ( A [,] B ) )
Theorem	lincmble 10417	A linear combination of two reals which lies in the interval between them. Like lincmb01cmp 10416 but generalized to require merely A <_ B not A < B. (Contributed by Jim Kingdon, 13-May-2026.)
|- ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) x. A ) + ( T x. B ) ) e. ( A [,] B ) )
Theorem	iccf1o 10418*	Describe a bijection from [ 0 , 1 ] to an arbitrary nontrivial closed interval [ A , B ]. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )   =>    |- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) /\ `' F = ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) ) )
Theorem	unitssre 10419	( 0 [,] 1 ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
|- ( 0 [,] 1 ) C_ RR
Theorem	iccen 10420	Any nontrivial closed interval is equinumerous to the unit interval. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 8-Sep-2015.)
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( 0 [,] 1 ) ~~ ( A [,] B ) )
Theorem	zltaddlt1le 10421	The sum of an integer and a real number between 0 and 1 is less than or equal to a second integer iff the sum is less than the second integer. (Contributed by AV, 1-Jul-2021.)
|- ( ( M e. ZZ /\ N e. ZZ /\ A e. ( 0 (,) 1 ) ) -> ( ( M + A ) < N <-> ( M + A ) <_ N ) )
4.5.4  Finite intervals of integers
Syntax	cfz 10422	Extend class notation to include the notation for a contiguous finite set of integers. Read " M ... N " as "the set of integers from M to N inclusive". This symbol is also used informally in some comments to denote an ellipsis, e.g., A + A ^ 2 + ... + A ^ ( N - 1 ).
class ...
Definition	df-fz 10423*	Define an operation that produces a finite set of sequential integers. Read " M ... N " as "the set of integers from M to N inclusive". See fzval 10424 for its value and additional comments. (Contributed by NM, 6-Sep-2005.)
|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
Theorem	fzval 10424*	The value of a finite set of sequential integers. E.g., 2 ... 5 means the set { 2 , 3 , 4 , 5 }. A special case of this definition (starting at 1) appears as Definition 11-2.1 of [Gleason] p. 141, where NNk means our 1 ... k; he calls these sets segments of the integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = { k e. ZZ | ( M <_ k /\ k <_ N ) } )
Theorem	fzval2 10425	An alternate way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = ( ( M [,] N ) i^i ZZ ) )
Theorem	fzf 10426	Establish the domain and codomain of the finite integer sequence function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 16-Nov-2013.)
|- ... : ( ZZ X. ZZ ) --> ~P ZZ
Theorem	elfz1 10427	Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( K e. ZZ /\ M <_ K /\ K <_ N ) ) )
Theorem	elfz 10428	Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( M <_ K /\ K <_ N ) ) )
Theorem	elfz2 10429	Membership in a finite set of sequential integers. We use the fact that an operation's value is empty outside of its domain to show M e. ZZ and N e. ZZ. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) )
Theorem	elfzd 10430	Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> M <_ K )   &    |- ( ph -> K <_ N )   =>    |- ( ph -> K e. ( M ... N ) )
Theorem	elfz5 10431	Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.)
|- ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> K <_ N ) )
Theorem	elfz4 10432	Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) -> K e. ( M ... N ) )
Theorem	elfzuzb 10433	Membership in a finite set of sequential integers in terms of sets of upper integers. (Contributed by NM, 18-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) )
Theorem	eluzfz 10434	Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ( K e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> K e. ( M ... N ) )
Theorem	elfzuz 10435	A member of a finite set of sequential integers belongs to an upper set of integers. (Contributed by NM, 17-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
Theorem	elfzuz3 10436	Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
Theorem	elfzel2 10437	Membership in a finite set of sequential integer implies the upper bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> N e. ZZ )
Theorem	elfzel1 10438	Membership in a finite set of sequential integer implies the lower bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> M e. ZZ )
Theorem	elfzelz 10439	A member of a finite set of sequential integer is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> K e. ZZ )
Theorem	elfzelzd 10440	A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> K e. ( M ... N ) )   =>    |- ( ph -> K e. ZZ )
Theorem	fzssz 10441	A finite sequence of integers is a set of integers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( M ... N ) C_ ZZ
Theorem	elfzle1 10442	A member of a finite set of sequential integer is greater than or equal to the lower bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> M <_ K )
Theorem	elfzle2 10443	A member of a finite set of sequential integer is less than or equal to the upper bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> K <_ N )
Theorem	elfzuz2 10444	Implication of membership in a finite set of sequential integers. (Contributed by NM, 20-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> N e. ( ZZ>= ` M ) )
Theorem	elfzle3 10445	Membership in a finite set of sequential integer implies the bounds are comparable. (Contributed by NM, 18-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> M <_ N )
Theorem	eluzfz1 10446	Membership in a finite set of sequential integers - special case. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
Theorem	eluzfz2 10447	Membership in a finite set of sequential integers - special case. (Contributed by NM, 13-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
Theorem	eluzfz2b 10448	Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.)
|- ( N e. ( ZZ>= ` M ) <-> N e. ( M ... N ) )
Theorem	elfz3 10449	Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.)
|- ( N e. ZZ -> N e. ( N ... N ) )
Theorem	elfz1eq 10450	Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.)
|- ( K e. ( N ... N ) -> K = N )
Theorem	elfzubelfz 10451	If there is a member in a finite set of sequential integers, the upper bound is also a member of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 31-May-2018.)
|- ( K e. ( M ... N ) -> N e. ( M ... N ) )
Theorem	peano2fzr 10452	A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.)
|- ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ... N ) ) -> K e. ( M ... N ) )
Theorem	fzm 10453*	Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.)
|- ( E. x x e. ( M ... N ) <-> N e. ( ZZ>= ` M ) )
Theorem	fztri3or 10454	Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K < M \/ K e. ( M ... N ) \/ N < K ) )
Theorem	fzdcel 10455	Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> DECID K e. ( M ... N ) )
Theorem	fznlem 10456	A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N < M -> ( M ... N ) = (/) ) )
Theorem	fzn 10457	A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N < M <-> ( M ... N ) = (/) ) )
Theorem	fzen 10458	A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.)
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M ... N ) ~~ ( ( M + K ) ... ( N + K ) ) )
Theorem	fz1n 10459	A 1-based finite set of sequential integers is empty iff it ends at index 0. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( N e. NN0 -> ( ( 1 ... N ) = (/) <-> N = 0 ) )
Theorem	0fz1 10460	Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.)
|- ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> ( F = (/) <-> N = 0 ) )
Theorem	fz10 10461	There are no integers between 1 and 0. (Contributed by Jeff Madsen, 16-Jun-2010.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
|- ( 1 ... 0 ) = (/)
Theorem	fz00m1 10462	There are no integers between 0 and minus 1. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( 0 ... ( 0 - 1 ) ) = (/)
Theorem	uzsubsubfz 10463	Membership of an integer greater than L decreased by ( L - M ) in an M based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.)
|- ( ( L e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` L ) ) -> ( N - ( L - M ) ) e. ( M ... N ) )
Theorem	uzsubsubfz1 10464	Membership of an integer greater than L decreased by ( L - 1 ) in a 1 based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.)
|- ( ( L e. NN /\ N e. ( ZZ>= ` L ) ) -> ( N - ( L - 1 ) ) e. ( 1 ... N ) )
Theorem	ige3m2fz 10465	Membership of an integer greater than 2 decreased by 2 in a 1 based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.)
|- ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. ( 1 ... N ) )
Theorem	fzsplit2 10466	Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( M ... N ) = ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) )
Theorem	fzsplit 10467	Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 13-Apr-2016.)
|- ( K e. ( M ... N ) -> ( M ... N ) = ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) )
Theorem	fzdisj 10468	Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( K < M -> ( ( J ... K ) i^i ( M ... N ) ) = (/) )
Theorem	fzsplit3 10469	Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.)
|- ( K e. ( M ... N ) -> ( M ... N ) = ( ( M ... ( K - 1 ) ) u. ( K ... N ) ) )
Theorem	fz01en 10470	0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.)
|- ( N e. ZZ -> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )
Theorem	elfznn 10471	A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005.)
|- ( K e. ( 1 ... N ) -> K e. NN )
Theorem	elfz1end 10472	A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. NN <-> A e. ( 1 ... A ) )
Theorem	fz1ssnn 10473	A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( 1 ... A ) C_ NN
Theorem	fznn0sub 10474	Subtraction closure for a member of a finite set of sequential integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> ( N - K ) e. NN0 )
Theorem	fzmmmeqm 10475	Subtracting the difference of a member of a finite range of integers and the lower bound of the range from the difference of the upper bound and the lower bound of the range results in the difference of the upper bound of the range and the member. (Contributed by Alexander van der Vekens, 27-May-2018.)
|- ( M e. ( L ... N ) -> ( ( N - L ) - ( M - L ) ) = ( N - M ) )
Theorem	fzaddel 10476	Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J e. ( M ... N ) <-> ( J + K ) e. ( ( M + K ) ... ( N + K ) ) ) )
Theorem	fzsubel 10477	Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( J e. ZZ /\ K e. ZZ ) ) -> ( J e. ( M ... N ) <-> ( J - K ) e. ( ( M - K ) ... ( N - K ) ) ) )
Theorem	fzopth 10478	A finite set of sequential integers can represent an ordered pair. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( N e. ( ZZ>= ` M ) -> ( ( M ... N ) = ( J ... K ) <-> ( M = J /\ N = K ) ) )
Theorem	fzass4 10479	Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( B e. ( A ... D ) /\ C e. ( B ... D ) ) <-> ( B e. ( A ... C ) /\ C e. ( A ... D ) ) )
Theorem	fzss1 10480	Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( ZZ>= ` M ) -> ( K ... N ) C_ ( M ... N ) )
Theorem	fzss2 10481	Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( N e. ( ZZ>= ` K ) -> ( M ... K ) C_ ( M ... N ) )
Theorem	fzssuz 10482	A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.)
|- ( M ... N ) C_ ( ZZ>= ` M )
Theorem	fzsn 10483	A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( M e. ZZ -> ( M ... M ) = { M } )
Theorem	fzssp1 10484	Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( M ... N ) C_ ( M ... ( N + 1 ) )
Theorem	fzssnn 10485	Finite sets of sequential integers starting from a natural are a subset of the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017.)
|- ( M e. NN -> ( M ... N ) C_ NN )
Theorem	fzsuc 10486	Join a successor to the end of a finite set of sequential integers. (Contributed by NM, 19-Jul-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( N e. ( ZZ>= ` M ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
Theorem	fzspl 10487	Split the last element of a finite set of sequential integers. More generic than fzsuc 10486. (Contributed by Thierry Arnoux, 7-Nov-2016.)
|- ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ... ( N - 1 ) ) u. { N } ) )
Theorem	fzpred 10488	Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.)
|- ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( { M } u. ( ( M + 1 ) ... N ) ) )
Theorem	fzpreddisj 10489	A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.)
|- ( N e. ( ZZ>= ` M ) -> ( { M } i^i ( ( M + 1 ) ... N ) ) = (/) )
Theorem	elfzp1 10490	Append an element to a finite set of sequential integers. (Contributed by NM, 19-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
|- ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... ( N + 1 ) ) <-> ( K e. ( M ... N ) \/ K = ( N + 1 ) ) ) )
Theorem	fzp1ss 10491	Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
Theorem	fzelp1 10492	Membership in a set of sequential integers with an appended element. (Contributed by NM, 7-Dec-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> K e. ( M ... ( N + 1 ) ) )
Theorem	fzp1elp1 10493	Add one to an element of a finite set of integers. (Contributed by Jeff Madsen, 6-Jun-2010.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( K e. ( M ... N ) -> ( K + 1 ) e. ( M ... ( N + 1 ) ) )
Theorem	fznatpl1 10494	Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.)
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( I + 1 ) e. ( 1 ... N ) )
Theorem	fzpr 10495	A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( M e. ZZ -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } )
Theorem	fztp 10496	A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 7-Mar-2014.)
|- ( M e. ZZ -> ( M ... ( M + 2 ) ) = { M , ( M + 1 ) , ( M + 2 ) } )
Theorem	fzsuc2 10497	Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014.)
|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M - 1 ) ) ) -> ( M ... ( N + 1 ) ) = ( ( M ... N ) u. { ( N + 1 ) } ) )
Theorem	fzp1disj 10498	( M ... ( N + 1 ) ) is the disjoint union of ( M ... N ) with { ( N + 1 ) }. (Contributed by Mario Carneiro, 7-Mar-2014.)
|- ( ( M ... N ) i^i { ( N + 1 ) } ) = (/)
Theorem	fzdifsuc 10499	Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.)
|- ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )
Theorem	fzprval 10500*	Two ways of defining the first two values of a sequence on NN. (Contributed by NM, 5-Sep-2011.)
|- ( A. x e. ( 1 ... 2 ) ( F ` x ) = if ( x = 1 , A , B ) <-> ( ( F ` 1 ) = A /\ ( F ` 2 ) = B ) )