P. 101 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10001-10100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	icc0r 10001	An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( B < A -> ( A [,] B ) = (/) ) )
Theorem	eliooxr 10002	An inhabited open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.)
|- ( A e. ( B (,) C ) -> ( B e. RR* /\ C e. RR* ) )
Theorem	eliooord 10003	Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- ( A e. ( B (,) C ) -> ( B < A /\ A < C ) )
Theorem	ubioc1 10004	The upper bound belongs to an open-below, closed-above interval. See ubicc2 10060. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B e. ( A (,] B ) )
Theorem	lbico1 10005	The lower bound belongs to a closed-below, open-above interval. See lbicc2 10059. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A e. ( A [,) B ) )
Theorem	iccleub 10006	An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> C <_ B )
Theorem	iccgelb 10007	An element of a closed interval is more than or equal to its lower bound (Contributed by Thierry Arnoux, 23-Dec-2016.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> A <_ C )
Theorem	elioo5 10008	Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A (,) B ) <-> ( A < C /\ C < B ) ) )
Theorem	elioo4g 10009	Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( C e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR ) /\ ( A < C /\ C < B ) ) )
Theorem	ioossre 10010	An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
|- ( A (,) B ) C_ RR
Theorem	elioc2 10011	Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|- ( ( A e. RR* /\ B e. RR ) -> ( C e. ( A (,] B ) <-> ( C e. RR /\ A < C /\ C <_ B ) ) )
Theorem	elico2 10012	Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)
|- ( ( A e. RR /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR /\ A <_ C /\ C < B ) ) )
Theorem	elicc2 10013	Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
Theorem	elicc2i 10014	Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.)
|- A e. RR   &    |- B e. RR   =>    |- ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) )
Theorem	elicc4 10015	Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )
Theorem	iccss 10016	Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 20-Feb-2015.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ C /\ D <_ B ) ) -> ( C [,] D ) C_ ( A [,] B ) )
Theorem	iccssioo 10017	Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A < C /\ D < B ) ) -> ( C [,] D ) C_ ( A (,) B ) )
Theorem	icossico 10018	Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Thierry Arnoux, 21-Sep-2017.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D <_ B ) ) -> ( C [,) D ) C_ ( A [,) B ) )
Theorem	iccss2 10019	Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) ) -> ( C [,] D ) C_ ( A [,] B ) )
Theorem	iccssico 10020	Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D < B ) ) -> ( C [,] D ) C_ ( A [,) B ) )
Theorem	iccssioo2 10021	Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
|- ( ( C e. ( A (,) B ) /\ D e. ( A (,) B ) ) -> ( C [,] D ) C_ ( A (,) B ) )
Theorem	iccssico2 10022	Condition for a closed interval to be a subset of a closed-below, open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
|- ( ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) -> ( C [,] D ) C_ ( A [,) B ) )
Theorem	ioomax 10023	The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.)
|- ( -oo (,) +oo ) = RR
Theorem	iccmax 10024	The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.)
|- ( -oo [,] +oo ) = RR*
Theorem	ioopos 10025	The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.)
|- ( 0 (,) +oo ) = { x e. RR | 0 < x }
Theorem	ioorp 10026	The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( 0 (,) +oo ) = RR+
Theorem	iooshf 10027	Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - B ) e. ( C (,) D ) <-> A e. ( ( C + B ) (,) ( D + B ) ) ) )
Theorem	iocssre 10028	A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
Theorem	icossre 10029	A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014.)
|- ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) C_ RR )
Theorem	iccssre 10030	A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
Theorem	iccssxr 10031	A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
|- ( A [,] B ) C_ RR*
Theorem	iocssxr 10032	An open-below, closed-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.)
|- ( A (,] B ) C_ RR*
Theorem	icossxr 10033	A closed-below, open-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.)
|- ( A [,) B ) C_ RR*
Theorem	ioossicc 10034	An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
|- ( A (,) B ) C_ ( A [,] B )
Theorem	icossicc 10035	A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.)
|- ( A [,) B ) C_ ( A [,] B )
Theorem	iocssicc 10036	A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.)
|- ( A (,] B ) C_ ( A [,] B )
Theorem	ioossico 10037	An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.)
|- ( A (,) B ) C_ ( A [,) B )
Theorem	iocssioo 10038	Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D < B ) ) -> ( C (,] D ) C_ ( A (,) B ) )
Theorem	icossioo 10039	Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A < C /\ D <_ B ) ) -> ( C [,) D ) C_ ( A (,) B ) )
Theorem	ioossioo 10040	Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D <_ B ) ) -> ( C (,) D ) C_ ( A (,) B ) )
Theorem	iccsupr 10041*	A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum. To be useful without excluded middle, we'll probably need to change not equal to apart, and perhaps make other changes, but the theorem does hold as stated here. (Contributed by Paul Chapman, 21-Jan-2008.)
|- ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) /\ C e. S ) -> ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S y <_ x ) )
Theorem	elioopnf 10042	Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( A e. RR* -> ( B e. ( A (,) +oo ) <-> ( B e. RR /\ A < B ) ) )
Theorem	elioomnf 10043	Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( A e. RR* -> ( B e. ( -oo (,) A ) <-> ( B e. RR /\ B < A ) ) )
Theorem	elicopnf 10044	Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( A e. RR -> ( B e. ( A [,) +oo ) <-> ( B e. RR /\ A <_ B ) ) )
Theorem	repos 10045	Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.)
|- ( A e. ( 0 (,) +oo ) <-> ( A e. RR /\ 0 < A ) )
Theorem	ioof 10046	The set of open intervals of extended reals maps to subsets of reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
|- (,) : ( RR* X. RR* ) --> ~P RR
Theorem	iccf 10047	The set of closed intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- [,] : ( RR* X. RR* ) --> ~P RR*
Theorem	unirnioo 10048	The union of the range of the open interval function. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
|- RR = U. ran (,)
Theorem	dfioo2 10049*	Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- (,) = ( x e. RR* , y e. RR* |-> { w e. RR | ( x < w /\ w < y ) } )
Theorem	ioorebasg 10050	Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) e. ran (,) )
Theorem	elrege0 10051	The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
|- ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )
Theorem	rge0ssre 10052	Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)
|- ( 0 [,) +oo ) C_ RR
Theorem	elxrge0 10053	Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A ) )
Theorem	0e0icopnf 10054	0 is a member of ( 0 [,) +oo ) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 e. ( 0 [,) +oo )
Theorem	0e0iccpnf 10055	0 is a member of ( 0 [,] +oo ) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 e. ( 0 [,] +oo )
Theorem	ge0addcl 10056	The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- ( ( A e. ( 0 [,) +oo ) /\ B e. ( 0 [,) +oo ) ) -> ( A + B ) e. ( 0 [,) +oo ) )
Theorem	ge0mulcl 10057	The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- ( ( A e. ( 0 [,) +oo ) /\ B e. ( 0 [,) +oo ) ) -> ( A x. B ) e. ( 0 [,) +oo ) )
Theorem	ge0xaddcl 10058	The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) -> ( A +e B ) e. ( 0 [,] +oo ) )
Theorem	lbicc2 10059	The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) (Revised by Mario Carneiro, 9-Sep-2015.)
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
Theorem	ubicc2 10060	The upper bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
Theorem	0elunit 10061	Zero is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
|- 0 e. ( 0 [,] 1 )
Theorem	1elunit 10062	One is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
|- 1 e. ( 0 [,] 1 )
Theorem	iooneg 10063	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 10064	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 10065	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 10066*	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 10067	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 10068	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 10069	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 10070	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 10071	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 10072	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 10073	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 10074	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 10075	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 10076	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 10077	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 10078	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	iccf1o 10079*	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 10080	( 0 [,] 1 ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
|- ( 0 [,] 1 ) C_ RR
Theorem	iccen 10081	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 10082	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 10083	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 10084*	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 10085 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 10085*	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 10086	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 10087	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 10088	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 10089	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 10090	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 10091	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 10092	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 10093	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 10094	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 10095	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 10096	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 10097	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 10098	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 10099	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 10100	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 )