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	elunitcn 13501	The closed unit interval is a subset of the set of the complex numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 21-Dec-2016.)
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈ ℂ)
Theorem	0elunit 13502	Zero is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ 0 ∈ (0[,]1)
Theorem	1elunit 13503	One is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ 1 ∈ (0[,]1)
Theorem	iooneg 13504	Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴(,)𝐵) ↔ -𝐶 ∈ (-𝐵(,)-𝐴)))
Theorem	iccneg 13505	Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ -𝐶 ∈ (-𝐵[,]-𝐴)))
Theorem	icoshft 13506	A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ (𝐴[,)𝐵) → (𝑋 + 𝐶) ∈ ((𝐴 + 𝐶)[,)(𝐵 + 𝐶))))
Theorem	icoshftf1o 13507*	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.)
⊢ 𝐹 = (𝑥 ∈ (𝐴[,)𝐵) ↦ (𝑥 + 𝐶))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐹:(𝐴[,)𝐵)–1-1-onto→((𝐴 + 𝐶)[,)(𝐵 + 𝐶)))
Theorem	icoun 13508	The union of two adjacent left-closed right-open real intervals is a left-closed right-open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,)𝐵) ∪ (𝐵[,)𝐶)) = (𝐴[,)𝐶))
Theorem	icodisj 13509	Adjacent left-closed right-open real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴[,)𝐵) ∩ (𝐵[,)𝐶)) = ∅)
Theorem	ioounsn 13510	The union of an open interval with its upper endpoint is a left-open right-closed interval. (Contributed by Jon Pennant, 8-Jun-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵))
Theorem	snunioo 13511	The closure of one end of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ({𝐴} ∪ (𝐴(,)𝐵)) = (𝐴[,)𝐵))
Theorem	snunico 13512	The closure of the open end of a right-open real interval. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴[,)𝐵) ∪ {𝐵}) = (𝐴[,]𝐵))
Theorem	snunioc 13513	The closure of the open end of a left-open real interval. (Contributed by Thierry Arnoux, 28-Mar-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ({𝐴} ∪ (𝐴(,]𝐵)) = (𝐴[,]𝐵))
Theorem	prunioo 13514	The closure of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
Theorem	ioodisj 13515	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.)
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) ∧ 𝐵 ≤ 𝐶) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = ∅)
Theorem	ioojoin 13516	Join two open intervals to create a third. (Contributed by NM, 11-Aug-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → (((𝐴(,)𝐵) ∪ {𝐵}) ∪ (𝐵(,)𝐶)) = (𝐴(,)𝐶))
Theorem	difreicc 13517	The class difference of ℝ and a closed interval. (Contributed by FL, 18-Jun-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (ℝ ∖ (𝐴[,]𝐵)) = ((-∞(,)𝐴) ∪ (𝐵(,)+∞)))
Theorem	iccsplit 13518	Split a closed interval into the union of two closed intervals. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐴[,]𝐵) = ((𝐴[,]𝐶) ∪ (𝐶[,]𝐵)))
Theorem	iccshftr 13519	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 + 𝑅) = 𝐶    &   ⊢ (𝐵 + 𝑅) = 𝐷    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 + 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	iccshftri 13520	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (𝐴 + 𝑅) = 𝐶    &   ⊢ (𝐵 + 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 + 𝑅) ∈ (𝐶[,]𝐷))
Theorem	iccshftl 13521	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 − 𝑅) = 𝐶    &   ⊢ (𝐵 − 𝑅) = 𝐷    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 − 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	iccshftli 13522	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (𝐴 − 𝑅) = 𝐶    &   ⊢ (𝐵 − 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 − 𝑅) ∈ (𝐶[,]𝐷))
Theorem	iccdil 13523	Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 · 𝑅) = 𝐶    &   ⊢ (𝐵 · 𝑅) = 𝐷    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 · 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	iccdili 13524	Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ+    &   ⊢ (𝐴 · 𝑅) = 𝐶    &   ⊢ (𝐵 · 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 · 𝑅) ∈ (𝐶[,]𝐷))
Theorem	icccntr 13525	Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 / 𝑅) = 𝐶    &   ⊢ (𝐵 / 𝑅) = 𝐷    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 / 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	icccntri 13526	Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ+    &   ⊢ (𝐴 / 𝑅) = 𝐶    &   ⊢ (𝐵 / 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 / 𝑅) ∈ (𝐶[,]𝐷))
Theorem	divelunit 13527	A condition for a ratio to be a member of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐴 / 𝐵) ∈ (0[,]1) ↔ 𝐴 ≤ 𝐵))
Theorem	lincmb01cmp 13528	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.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) ∈ (𝐴[,]𝐵))
Theorem	iccf1o 13529*	Describe a bijection from [0, 1] to an arbitrary nontrivial closed interval [𝐴, 𝐵]. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐹:(0[,]1)–1-1-onto→(𝐴[,]𝐵) ∧ ◡𝐹 = (𝑦 ∈ (𝐴[,]𝐵) ↦ ((𝑦 − 𝐴) / (𝐵 − 𝐴)))))
Theorem	iccen 13530	Any nontrivial closed interval is equinumerous to the unit interval. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 8-Sep-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (0[,]1) ≈ (𝐴[,]𝐵))
Theorem	xov1plusxeqvd 13531	A complex number 𝑋 is positive real iff 𝑋 / (1 + 𝑋) is in (0(,)1). Deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ -1)    ⇒   ⊢ (𝜑 → (𝑋 ∈ ℝ+ ↔ (𝑋 / (1 + 𝑋)) ∈ (0(,)1)))
Theorem	unitssre 13532	(0[,]1) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
⊢ (0[,]1) ⊆ ℝ
Theorem	unitsscn 13533	The closed unit interval is a subset of the set of the complex numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016.)
⊢ (0[,]1) ⊆ ℂ
Theorem	supicc 13534	Supremum of a bounded set of real numbers. (Contributed by Thierry Arnoux, 17-May-2019.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶))    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶))
Theorem	supiccub 13535	The supremum of a bounded set of real numbers is an upper bound. (Contributed by Thierry Arnoux, 20-May-2019.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶))    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐷 ≤ sup(𝐴, ℝ, < ))
Theorem	supicclub 13536*	The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶))    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐷 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐷 < 𝑧))
Theorem	supicclub2 13537*	The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶))    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ≤ 𝐷)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐷)
Theorem	zltaddlt1le 13538	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)) → ((𝑀 + 𝐴) < 𝑁 ↔ (𝑀 + 𝐴) ≤ 𝑁))
Theorem	xnn0xrge0 13539	An extended nonnegative integer is an extended nonnegative real. (Contributed by AV, 10-Dec-2020.)
⊢ (𝐴 ∈ ℕ0* → 𝐴 ∈ (0[,]+∞))
Theorem	nnge2recico01 13540	The reciprocal of an integer greater than 1 is in the right open interval between 0 and 1. (Contributed by AV, 10-Apr-2026.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (1 / 𝑁) ∈ (0[,)1))
5.5.5  Finite intervals of integers
Syntax	cfz 13541	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 13542*	Define an operation that produces a finite set of sequential integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive". See fzval 13543 for its value and additional comments. (Contributed by NM, 6-Sep-2005.)
⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)})
Theorem	fzval 13543*	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 13544	An alternative way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ))
Theorem	fzf 13545	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 13546	Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
Theorem	elfz 13547	Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
Theorem	elfz2 13548	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 13549	Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfz5 13550	Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.)
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾 ≤ 𝑁))
Theorem	elfz4 13551	Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfzuzb 13552	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 13553	Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfzuz 13554	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 13555	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 13556	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 13557	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 13558	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 13559	A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → 𝐾 ∈ ℤ)
Theorem	fzssz 13560	A finite sequence of integers is a set of integers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝑀...𝑁) ⊆ ℤ
Theorem	elfzle1 13561	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 13562	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 13563	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 13564	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 13565	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 13566	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 13567	Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑁 ∈ (𝑀...𝑁))
Theorem	elfz3 13568	Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.)
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (𝑁...𝑁))
Theorem	elfz1eq 13569	Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.)
⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁)
Theorem	elfzubelfz 13570	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 13571	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 13572	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 13573	A finite set of sequential integers is empty if its bounds are not integers. (Contributed by AV, 13-Oct-2018.)
⊢ ((𝑀 ∉ ℤ ∨ 𝑁 ∉ ℤ) → (𝑀...𝑁) = ∅)
Theorem	fzn 13574	A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅))
Theorem	fzen 13575	A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))
Theorem	fz1n 13576	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 13577	0 is not an element of a finite interval of integers starting at 1. (Contributed by AV, 27-Aug-2020.)
⊢ 0 ∉ (1...𝑁)
Theorem	0fz1 13578	Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (1...𝑁)) → (𝐹 = ∅ ↔ 𝑁 = 0))
Theorem	fz10 13579	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 13580	There are no integers between 0 and minus 1. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ (0...(0 − 1)) = ∅
Theorem	uzsubsubfz 13581	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 13582	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 13583	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 13584	Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)))
Theorem	fzsplit 13585	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 13586	Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)
Theorem	fz01en 13587	0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁))
Theorem	elfznn 13588	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 13589	A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴))
Theorem	fz1ssnn 13590	A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (1...𝐴) ⊆ ℕ
Theorem	fznn0sub 13591	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 13592	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 13593	Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
Theorem	fzadd2 13594	Membership of a sum in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ)) → ((𝐽 ∈ (𝑀...𝑁) ∧ 𝐾 ∈ (𝑂...𝑃)) → (𝐽 + 𝐾) ∈ ((𝑀 + 𝑂)...(𝑁 + 𝑃))))
Theorem	fzsubel 13595	Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾))))
Theorem	fzopth 13596	A finite set of sequential integers has the ordered pair property (compare opth 5457) under certain conditions. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾)))
Theorem	fzass4 13597	Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐵 ∈ (𝐴...𝐷) ∧ 𝐶 ∈ (𝐵...𝐷)) ↔ (𝐵 ∈ (𝐴...𝐶) ∧ 𝐶 ∈ (𝐴...𝐷)))
Theorem	fzss1 13598	Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁))
Theorem	fzss2 13599	Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁))
Theorem	fzssuz 13600	A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.)
⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀)