P. 102 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10101-10200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zltaddlt1le 10101	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.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ (0(,)1)) → ((𝑀 + 𝐴) < 𝑁 ↔ (𝑀 + 𝐴) ≤ 𝑁))
4.5.4  Finite intervals of integers
Syntax	cfz 10102	Extend class notation to include the notation for a contiguous finite set of integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive". This symbol is also used informally in some comments to denote an ellipsis, e.g., 𝐴 + 𝐴↑2 + ... + 𝐴↑(𝑁 − 1).
class ...
Definition	df-fz 10103*	Define an operation that produces a finite set of sequential integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive". See fzval 10104 for its value and additional comments. (Contributed by NM, 6-Sep-2005.)
⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)})
Theorem	fzval 10104*	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 ℕk means our 1...𝑘; he calls these sets segments of the integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = {𝑘 ∈ ℤ ∣ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)})
Theorem	fzval2 10105	An alternate way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ))
Theorem	fzf 10106	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.)
⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
Theorem	elfz1 10107	Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
Theorem	elfz 10108	Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
Theorem	elfz2 10109	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 𝑀 ∈ ℤ and 𝑁 ∈ ℤ. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
Theorem	elfzd 10110	Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfz5 10111	Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.)
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾 ≤ 𝑁))
Theorem	elfz4 10112	Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfzuzb 10113	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
Theorem	eluzfz 10114	Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfzuz 10115	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 10116	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 10117	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 10118	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 10119	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.)
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
Theorem	elfzelzd 10120	A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → 𝐾 ∈ ℤ)
Theorem	elfzle1 10121	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 10122	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 10123	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 10124	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 10125	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 10126	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 10127	Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑁 ∈ (𝑀...𝑁))
Theorem	elfz3 10128	Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.)
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (𝑁...𝑁))
Theorem	elfz1eq 10129	Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.)
⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁)
Theorem	elfzubelfz 10130	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 10131	A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.)
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ (𝐾 + 1) ∈ (𝑀...𝑁)) → 𝐾 ∈ (𝑀...𝑁))
Theorem	fzm 10132*	Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.)
⊢ (∃𝑥 𝑥 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (ℤ≥‘𝑀))
Theorem	fztri3or 10133	Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾))
Theorem	fzdcel 10134	Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝐾 ∈ (𝑀...𝑁))
Theorem	fznlem 10135	A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 → (𝑀...𝑁) = ∅))
Theorem	fzn 10136	A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅))
Theorem	fzen 10137	A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))
Theorem	fz1n 10138	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	0fz1 10139	Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (1...𝑁)) → (𝐹 = ∅ ↔ 𝑁 = 0))
Theorem	fz10 10140	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 10141	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 10142	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 10143	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 10144	Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)))
Theorem	fzsplit 10145	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 10146	Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)
Theorem	fz01en 10147	0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁))
Theorem	elfznn 10148	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 10149	A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴))
Theorem	fz1ssnn 10150	A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (1...𝐴) ⊆ ℕ
Theorem	fznn0sub 10151	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 10152	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 10153	Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
Theorem	fzsubel 10154	Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾))))
Theorem	fzopth 10155	A finite set of sequential integers can represent an ordered pair. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾)))
Theorem	fzass4 10156	Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐵 ∈ (𝐴...𝐷) ∧ 𝐶 ∈ (𝐵...𝐷)) ↔ (𝐵 ∈ (𝐴...𝐶) ∧ 𝐶 ∈ (𝐴...𝐷)))
Theorem	fzss1 10157	Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁))
Theorem	fzss2 10158	Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))
Theorem	fzssuz 10159	A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.)
⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀)
Theorem	fzsn 10160	A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
Theorem	fzssp1 10161	Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
Theorem	fzssnn 10162	Finite sets of sequential integers starting from a natural are a subset of the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017.)
⊢ (𝑀 ∈ ℕ → (𝑀...𝑁) ⊆ ℕ)
Theorem	fzsuc 10163	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 10164	Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁)))
Theorem	fzpreddisj 10165	A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ({𝑀} ∩ ((𝑀 + 1)...𝑁)) = ∅)
Theorem	elfzp1 10166	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 10167	Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁))
Theorem	fzelp1 10168	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 10169	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 10170	Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁))
Theorem	fzpr 10171	A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
Theorem	fztp 10172	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	fzsuc2 10173	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 10174	(𝑀...(𝑁 + 1)) is the disjoint union of (𝑀...𝑁) with {(𝑁 + 1)}. (Contributed by Mario Carneiro, 7-Mar-2014.)
⊢ ((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅
Theorem	fzdifsuc 10175	Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)}))
Theorem	fzprval 10176*	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 10177*	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 10178	Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)) ↔ (𝐽 − 𝐾) ∈ (𝑀...𝑁)))
Theorem	fzrev2 10179	Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀))))
Theorem	fzrev2i 10180	Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)))
Theorem	fzrev3 10181	The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.)
⊢ (𝐾 ∈ ℤ → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁)))
Theorem	fzrev3i 10182	The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.)
⊢ (𝐾 ∈ (𝑀...𝑁) → ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁))
Theorem	fznn 10183	Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
Theorem	elfz1b 10184	Membership in a 1 based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.)
⊢ (𝑁 ∈ (1...𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ≤ 𝑀))
Theorem	elfzm11 10185	Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁)))
Theorem	uzsplit 10186	Express an upper integer set as the disjoint (see uzdisj 10187) union of the first 𝑁 values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑀) = ((𝑀...(𝑁 − 1)) ∪ (ℤ≥‘𝑁)))
Theorem	uzdisj 10187	The first 𝑁 elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.)
⊢ ((𝑀...(𝑁 − 1)) ∩ (ℤ≥‘𝑁)) = ∅
Theorem	fseq1p1m1 10188	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 10189	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 10190*	Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.)
⊢ (𝑁 ∈ ℤ → (∀𝑘 ∈ (𝑁...𝑁)𝜑 ↔ [𝑁 / 𝑘]𝜑))
Theorem	elfzp1b 10191	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 10192	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 10193	Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁))))
Theorem	fzm1 10194	Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)))
Theorem	fzneuz 10195	No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.)
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → ¬ (𝑀...𝑁) = (ℤ≥‘𝐾))
Theorem	fznuz 10196	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 10197	Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.)
⊢ (𝐾 ∈ (ℤ≥‘𝑁) → ¬ 𝐾 ∈ (𝑀...(𝑁 − 1)))
Theorem	fzp1nel 10198	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 10199*	Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))[(𝐾 − 𝑘) / 𝑗]𝜑))
Theorem	fzrevral2 10200*	Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[(𝐾 − 𝑘) / 𝑗]𝜑))