P. 104 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10301-10400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ioossico 10301	An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.)
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,)𝐵)
Theorem	iocssioo 10302	Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶(,]𝐷) ⊆ (𝐴(,)𝐵))
Theorem	icossioo 10303	Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴(,)𝐵))
Theorem	ioossioo 10304	Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))
Theorem	iccsupr 10305*	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.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑆 ⊆ (𝐴[,]𝐵) ∧ 𝐶 ∈ 𝑆) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥))
Theorem	elioopnf 10306	Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)))
Theorem	elioomnf 10307	Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝐴)))
Theorem	elicopnf 10308	Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)))
Theorem	repos 10309	Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.)
⊢ (𝐴 ∈ (0(,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	ioof 10310	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.)
⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
Theorem	iccf 10311	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.)
⊢ [,]:(ℝ* × ℝ*)⟶𝒫 ℝ*
Theorem	unirnioo 10312	The union of the range of the open interval function. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
⊢ ℝ = ∪ ran (,)
Theorem	dfioo2 10313*	Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑤 ∈ ℝ ∣ (𝑥 < 𝑤 ∧ 𝑤 < 𝑦)})
Theorem	ioorebasg 10314	Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) ∈ ran (,))
Theorem	elrege0 10315	The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Theorem	rge0ssre 10316	Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)
⊢ (0[,)+∞) ⊆ ℝ
Theorem	elxrge0 10317	Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))
Theorem	0e0icopnf 10318	0 is a member of (0[,)+∞) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ∈ (0[,)+∞)
Theorem	0e0iccpnf 10319	0 is a member of (0[,]+∞) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ∈ (0[,]+∞)
Theorem	ge0addcl 10320	The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 + 𝐵) ∈ (0[,)+∞))
Theorem	ge0mulcl 10321	The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 · 𝐵) ∈ (0[,)+∞))
Theorem	ge0xaddcl 10322	The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 +𝑒 𝐵) ∈ (0[,]+∞))
Theorem	lbicc2 10323	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.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
Theorem	ubicc2 10324	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.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
Theorem	0elunit 10325	Zero is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ 0 ∈ (0[,]1)
Theorem	1elunit 10326	One is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ 1 ∈ (0[,]1)
Theorem	iooneg 10327	Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴(,)𝐵) ↔ -𝐶 ∈ (-𝐵(,)-𝐴)))
Theorem	iccneg 10328	Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ -𝐶 ∈ (-𝐵[,]-𝐴)))
Theorem	icoshft 10329	A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ (𝐴[,)𝐵) → (𝑋 + 𝐶) ∈ ((𝐴 + 𝐶)[,)(𝐵 + 𝐶))))
Theorem	icoshftf1o 10330*	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	icodisj 10331	End-to-end closed-below, open-above real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴[,)𝐵) ∩ (𝐵[,)𝐶)) = ∅)
Theorem	ioodisj 10332	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	iccshftr 10333	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 + 𝑅) = 𝐶    &   ⊢ (𝐵 + 𝑅) = 𝐷    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 + 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	iccshftri 10334	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (𝐴 + 𝑅) = 𝐶    &   ⊢ (𝐵 + 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 + 𝑅) ∈ (𝐶[,]𝐷))
Theorem	iccshftl 10335	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 − 𝑅) = 𝐶    &   ⊢ (𝐵 − 𝑅) = 𝐷    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 − 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	iccshftli 10336	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (𝐴 − 𝑅) = 𝐶    &   ⊢ (𝐵 − 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 − 𝑅) ∈ (𝐶[,]𝐷))
Theorem	iccdil 10337	Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 · 𝑅) = 𝐶    &   ⊢ (𝐵 · 𝑅) = 𝐷    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 · 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	iccdili 10338	Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ+    &   ⊢ (𝐴 · 𝑅) = 𝐶    &   ⊢ (𝐵 · 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 · 𝑅) ∈ (𝐶[,]𝐷))
Theorem	icccntr 10339	Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 / 𝑅) = 𝐶    &   ⊢ (𝐵 / 𝑅) = 𝐷    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 / 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	icccntri 10340	Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ+    &   ⊢ (𝐴 / 𝑅) = 𝐶    &   ⊢ (𝐵 / 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝑋 / 𝑅) ∈ (𝐶[,]𝐷))
Theorem	divelunit 10341	A condition for a ratio to be a member of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐴 / 𝐵) ∈ (0[,]1) ↔ 𝐴 ≤ 𝐵))
Theorem	lincmb01cmp 10342	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	lincmble 10343	A linear combination of two reals which lies in the interval between them. Like lincmb01cmp 10342 but generalized to require merely 𝐴 ≤ 𝐵 not 𝐴 < 𝐵. (Contributed by Jim Kingdon, 13-May-2026.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) ∈ (𝐴[,]𝐵))
Theorem	iccf1o 10344*	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	unitssre 10345	(0[,]1) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
⊢ (0[,]1) ⊆ ℝ
Theorem	iccen 10346	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	zltaddlt1le 10347	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 10348	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 10349*	Define an operation that produces a finite set of sequential integers. Read "𝑀...𝑁 " as "the set of integers from 𝑀 to 𝑁 inclusive". See fzval 10350 for its value and additional comments. (Contributed by NM, 6-Sep-2005.)
⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)})
Theorem	fzval 10350*	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 10351	An alternate way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ))
Theorem	fzf 10352	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 10353	Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
Theorem	elfz 10354	Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
Theorem	elfz2 10355	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 10356	Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfz5 10357	Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.)
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾 ≤ 𝑁))
Theorem	elfz4 10358	Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfzuzb 10359	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 10360	Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfzuz 10361	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 10362	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 10363	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 10364	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 10365	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 10366	A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → 𝐾 ∈ ℤ)
Theorem	elfzle1 10367	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 10368	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 10369	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 10370	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 10371	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 10372	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 10373	Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑁 ∈ (𝑀...𝑁))
Theorem	elfz3 10374	Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.)
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (𝑁...𝑁))
Theorem	elfz1eq 10375	Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.)
⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁)
Theorem	elfzubelfz 10376	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 10377	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 10378*	Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.)
⊢ (∃𝑥 𝑥 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (ℤ≥‘𝑀))
Theorem	fztri3or 10379	Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾))
Theorem	fzdcel 10380	Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝐾 ∈ (𝑀...𝑁))
Theorem	fznlem 10381	A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 → (𝑀...𝑁) = ∅))
Theorem	fzn 10382	A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅))
Theorem	fzen 10383	A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))
Theorem	fz1n 10384	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 10385	Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (1...𝑁)) → (𝐹 = ∅ ↔ 𝑁 = 0))
Theorem	fz10 10386	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 10387	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 10388	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 10389	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 10390	Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (((𝐾 + 1) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁)))
Theorem	fzsplit 10391	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 10392	Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)
Theorem	fz01en 10393	0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.)
⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁))
Theorem	elfznn 10394	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 10395	A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴))
Theorem	fz1ssnn 10396	A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (1...𝐴) ⊆ ℕ
Theorem	fznn0sub 10397	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 10398	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 10399	Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))))
Theorem	fzsubel 10400	Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾))))