P. 136 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13501-13600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eluzfz 13501	Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfzuz 13502	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
Theorem	elfzuz3 13503	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
Theorem	elfzel2 13504	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)
Theorem	elfzel1 13505	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
Theorem	elfzelz 13506	A member of a finite set of sequential integers is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
Theorem	elfzelzd 13507	A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → 𝐾 ∈ ℤ)
Theorem	fzssz 13508	A finite sequence of integers is a set of integers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝑀...𝑁) ⊆ ℤ
Theorem	elfzle1 13509	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾)
Theorem	elfzle2 13510	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁)
Theorem	elfzuz2 13511	Implication of membership in a finite set of sequential integers. (Contributed by NM, 20-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑀))
Theorem	elfzle3 13512	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑁)
Theorem	eluzfz1 13513	Membership in a finite set of sequential integers - special case. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))
Theorem	eluzfz2 13514	Membership in a finite set of sequential integers - special case. (Contributed by NM, 13-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
Theorem	eluzfz2b 13515	Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑁 ∈ (𝑀...𝑁))
Theorem	elfz3 13516	Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.)
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (𝑁...𝑁))
Theorem	elfz1eq 13517	Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.)
⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁)
Theorem	elfzubelfz 13518	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (𝑀...𝑁))
Theorem	peano2fzr 13519	A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.)
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ (𝐾 + 1) ∈ (𝑀...𝑁)) → 𝐾 ∈ (𝑀...𝑁))
Theorem	fzn0 13520	Properties of a finite interval of integers which is nonempty. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
Theorem	fz0 13521	A finite set of sequential integers is empty if its bounds are not integers. (Contributed by AV, 13-Oct-2018.)
⊢ ((𝑀 ∉ ℤ ∨ 𝑁 ∉ ℤ) → (𝑀...𝑁) = ∅)
Theorem	fzn 13522	A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅))
Theorem	fzen 13523	A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))
Theorem	fz1n 13524	A 1-based finite set of sequential integers is empty iff it ends at index 0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑁 ∈ ℕ0 → ((1...𝑁) = ∅ ↔ 𝑁 = 0))
Theorem	0nelfz1 13525	0 is not an element of a finite interval of integers starting at 1. (Contributed by AV, 27-Aug-2020.)
⊢ 0 ∉ (1...𝑁)
Theorem	0fz1 13526	Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (1...𝑁)) → (𝐹 = ∅ ↔ 𝑁 = 0))
Theorem	fz10 13527	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	uzsubsubfz 13528	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.)
⊢ ((𝐿 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐿)) → (𝑁 − (𝐿 − 𝑀)) ∈ (𝑀...𝑁))
Theorem	uzsubsubfz1 13529	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.)
⊢ ((𝐿 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝐿)) → (𝑁 − (𝐿 − 1)) ∈ (1...𝑁))
Theorem	ige3m2fz 13530	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.)
⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑁 − 2) ∈ (1...𝑁))
Theorem	fzsplit2 13531	Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)))
Theorem	fzsplit 13532	Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 13-Apr-2016.)
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)))
Theorem	fzdisj 13533	Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)
Theorem	fz01en 13534	0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁))
Theorem	elfznn 13535	A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005.)
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
Theorem	elfz1end 13536	A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴))
Theorem	fz1ssnn 13537	A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (1...𝐴) ⊆ ℕ
Theorem	fznn0sub 13538	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑁 − 𝐾) ∈ ℕ0)
Theorem	fzmmmeqm 13539	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.)
⊢ (𝑀 ∈ (𝐿...𝑁) → ((𝑁 − 𝐿) − (𝑀 − 𝐿)) = (𝑁 − 𝑀))
Theorem	fzaddel 13540	Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
Theorem	fzadd2 13541	Membership of a sum in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ)) → ((𝐽 ∈ (𝑀...𝑁) ∧ 𝐾 ∈ (𝑂...𝑃)) → (𝐽 + 𝐾) ∈ ((𝑀 + 𝑂)...(𝑁 + 𝑃))))
Theorem	fzsubel 13542	Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾))))
Theorem	fzopth 13543	A finite set of sequential integers has the ordered pair property (compare opth 5477) under certain conditions. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾)))
Theorem	fzass4 13544	Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐵 ∈ (𝐴...𝐷) ∧ 𝐶 ∈ (𝐵...𝐷)) ↔ (𝐵 ∈ (𝐴...𝐶) ∧ 𝐶 ∈ (𝐴...𝐷)))
Theorem	fzss1 13545	Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁))
Theorem	fzss2 13546	Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))
Theorem	fzssuz 13547	A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.)
⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀)
Theorem	fzsn 13548	A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
Theorem	fzssp1 13549	Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
Theorem	fzssnn 13550	Finite sets of sequential integers starting from a natural are a subset of the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017.)
⊢ (𝑀 ∈ ℕ → (𝑀...𝑁) ⊆ ℕ)
Theorem	ssfzunsnext 13551	A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 13-Nov-2021.)
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑆 ∪ {𝐼}) ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))
Theorem	ssfzunsn 13552	A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 8-Jun-2021.) (Proof shortened by AV, 13-Nov-2021.)
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝑆 ∪ {𝐼}) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))
Theorem	fzsuc 13553	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.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)}))
Theorem	fzpred 13554	Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁)))
Theorem	fzpreddisj 13555	A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ({𝑀} ∩ ((𝑀 + 1)...𝑁)) = ∅)
Theorem	elfzp1 13556	Append an element to a finite set of sequential integers. (Contributed by NM, 19-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1))))
Theorem	fzp1ss 13557	Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁))
Theorem	fzelp1 13558	Membership in a set of sequential integers with an appended element. (Contributed by NM, 7-Dec-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (𝑀...(𝑁 + 1)))
Theorem	fzp1elp1 13559	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝐾 + 1) ∈ (𝑀...(𝑁 + 1)))
Theorem	fznatpl1 13560	Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁))
Theorem	fzpr 13561	A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
Theorem	fztp 13562	A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 7-Mar-2014.)
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 2)) = {𝑀, (𝑀 + 1), (𝑀 + 2)})
Theorem	fz12pr 13563	An integer range between 1 and 2 is a pair. (Contributed by AV, 11-Jan-2023.)
⊢ (1...2) = {1, 2}
Theorem	fzsuc2 13564	Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)}))
Theorem	fzp1disj 13565	(𝑀...(𝑁 + 1)) is the disjoint union of (𝑀...𝑁) with {(𝑁 + 1)}. (Contributed by Mario Carneiro, 7-Mar-2014.)
⊢ ((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅
Theorem	fzdifsuc 13566	Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)}))
Theorem	fzprval 13567*	Two ways of defining the first two values of a sequence on ℕ. (Contributed by NM, 5-Sep-2011.)
⊢ (∀𝑥 ∈ (1...2)(𝐹‘𝑥) = if(𝑥 = 1, 𝐴, 𝐵) ↔ ((𝐹‘1) = 𝐴 ∧ (𝐹‘2) = 𝐵))
Theorem	fztpval 13568*	Two ways of defining the first three values of a sequence on ℕ. (Contributed by NM, 13-Sep-2011.)
⊢ (∀𝑥 ∈ (1...3)(𝐹‘𝑥) = if(𝑥 = 1, 𝐴, if(𝑥 = 2, 𝐵, 𝐶)) ↔ ((𝐹‘1) = 𝐴 ∧ (𝐹‘2) = 𝐵 ∧ (𝐹‘3) = 𝐶))
Theorem	fzrev 13569	Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)) ↔ (𝐽 − 𝐾) ∈ (𝑀...𝑁)))
Theorem	fzrev2 13570	Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀))))
Theorem	fzrev2i 13571	Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)))
Theorem	fzrev3 13572	The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.)
⊢ (𝐾 ∈ ℤ → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁)))
Theorem	fzrev3i 13573	The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.)
⊢ (𝐾 ∈ (𝑀...𝑁) → ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁))
Theorem	fznn 13574	Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
Theorem	elfz1b 13575	Membership in a 1-based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) (Proof shortened by AV, 23-Jan-2022.)
⊢ (𝑁 ∈ (1...𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ≤ 𝑀))
Theorem	elfz1uz 13576	Membership in a 1-based finite set of sequential integers with an upper integer. (Contributed by AV, 23-Jan-2022.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (1...𝑀))
Theorem	elfzm11 13577	Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁)))
Theorem	uzsplit 13578	Express an upper integer set as the disjoint (see uzdisj 13579) union of the first 𝑁 values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑀) = ((𝑀...(𝑁 − 1)) ∪ (ℤ≥‘𝑁)))
Theorem	uzdisj 13579	The first 𝑁 elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.)
⊢ ((𝑀...(𝑁 − 1)) ∩ (ℤ≥‘𝑁)) = ∅
Theorem	fseq1p1m1 13580	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.)
⊢ 𝐻 = {⟨(𝑁 + 1), 𝐵⟩}    ⇒   ⊢ (𝑁 ∈ ℕ0 → ((𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻)) ↔ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁)))))
Theorem	fseq1m1p1 13581	Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ 𝐻 = {⟨𝑁, 𝐵⟩}    ⇒   ⊢ (𝑁 ∈ ℕ → ((𝐹:(1...(𝑁 − 1))⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻)) ↔ (𝐺:(1...𝑁)⟶𝐴 ∧ (𝐺‘𝑁) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...(𝑁 − 1))))))
Theorem	fz1sbc 13582*	Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.)
⊢ (𝑁 ∈ ℤ → (∀𝑘 ∈ (𝑁...𝑁)𝜑 ↔ [𝑁 / 𝑘]𝜑))
Theorem	elfzp1b 13583	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 13584	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 13585	Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁))))
Theorem	fzm1 13586	Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)))
Theorem	fzneuz 13587	No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.)
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → ¬ (𝑀...𝑁) = (ℤ≥‘𝐾))
Theorem	fznuz 13588	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 13589	Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.)
⊢ (𝐾 ∈ (ℤ≥‘𝑁) → ¬ 𝐾 ∈ (𝑀...(𝑁 − 1)))
Theorem	fzp1nel 13590	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 13591*	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 13592*	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 13593*	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 13594*	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 13595	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 13596	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...𝑁))
5.5.6  Finite intervals of nonnegative integers 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 13597	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 13598	Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.)
⊢ (𝑁 ∈ ℕ0 → (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁)))
Theorem	elfznn0 13599	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 13600	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)