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	nnsplit 10301	Express the set of positive integers as the disjoint union of the first 𝑁 values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝑁 ∈ ℕ → ℕ = ((1...𝑁) ∪ (ℤ≥‘(𝑁 + 1))))
Theorem	nn0disj 10302	The first 𝑁 + 1 elements of the set of nonnegative integers are distinct from any later members. (Contributed by AV, 8-Nov-2019.)
⊢ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅
Theorem	1fv 10303	A function on a singleton. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑃 = {⟨0, 𝑁⟩}) → (𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁))
Theorem	4fvwrd4 10304*	The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017.)
⊢ ((𝐿 ∈ (ℤ≥‘3) ∧ 𝑃:(0...𝐿)⟶𝑉) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 (((𝑃‘0) = 𝑎 ∧ (𝑃‘1) = 𝑏) ∧ ((𝑃‘2) = 𝑐 ∧ (𝑃‘3) = 𝑑)))
Theorem	2ffzeq 10305*	Two functions over 0 based finite set of sequential integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 30-Jun-2018.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝐹:(0...𝑀)⟶𝑋 ∧ 𝑃:(0...𝑁)⟶𝑌) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0...𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
4.5.6  Half-open integer ranges
Syntax	cfzo 10306	Syntax for half-open integer ranges.
class ..^
Definition	df-fzo 10307*	Define a function generating sets of integers using a half-open range. Read (𝑀..^𝑁) as the integers from 𝑀 up to, but not including, 𝑁; contrast with (𝑀...𝑁) df-fz 10173, which includes 𝑁. Not including the endpoint simplifies a number of formulas related to cardinality and splitting; contrast fzosplit 10343 with fzsplit 10215, for instance. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
Theorem	fzof 10308	Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
Theorem	elfzoel1 10309	Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
Theorem	elfzoel2 10310	Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
Theorem	elfzoelz 10311	Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)
Theorem	fzoval 10312	Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
Theorem	elfzo 10313	Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁)))
Theorem	elfzo2 10314	Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁))
Theorem	elfzouz 10315	Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
Theorem	nelfzo 10316	An integer not being a member of a half-open finite set of integers. (Contributed by AV, 29-Apr-2020.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∉ (𝑀..^𝑁) ↔ (𝐾 < 𝑀 ∨ 𝑁 ≤ 𝐾)))
Theorem	fzodcel 10317	Decidability of membership in a half-open integer interval. (Contributed by Jim Kingdon, 25-Aug-2022.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝐾 ∈ (𝑀..^𝑁))
Theorem	fzolb 10318	The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with 𝑀 < 𝑁. This provides an alternate notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate 𝑀 ∈ (ℤ≥‘𝑁). (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))
Theorem	fzolb2 10319	The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with 𝑀 < 𝑁. This provides an alternate notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate 𝑀 ∈ (ℤ≥‘𝑁). (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (𝑀..^𝑁) ↔ 𝑀 < 𝑁))
Theorem	elfzole1 10320	A member in a half-open integer interval is greater than or equal to the lower bound. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝐾)
Theorem	elfzolt2 10321	A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 < 𝑁)
Theorem	elfzolt3 10322	Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 < 𝑁)
Theorem	elfzolt2b 10323	A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝐾..^𝑁))
Theorem	elfzolt3b 10324	Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 ∈ (𝑀..^𝑁))
Theorem	fzonel 10325	A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ ¬ 𝐵 ∈ (𝐴..^𝐵)
Theorem	elfzouz2 10326	The upper bound of a half-open range is greater or equal to an element of the range. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
Theorem	elfzofz 10327	A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝑀...𝑁))
Theorem	elfzo3 10328	Express membership in a half-open integer interval in terms of the "less than or equal" and "less than" predicates on integers, resp. 𝐾 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝐾, 𝐾 ∈ (𝐾..^𝑁) ↔ 𝐾 < 𝑁. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ (𝐾..^𝑁)))
Theorem	fzom 10329*	A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.)
⊢ (∃𝑥 𝑥 ∈ (𝑀..^𝑁) ↔ 𝑀 ∈ (𝑀..^𝑁))
Theorem	fzossfz 10330	A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐴..^𝐵) ⊆ (𝐴...𝐵)
Theorem	fzon 10331	A half-open set of sequential integers is empty if the bounds are equal or reversed. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
Theorem	fzo0n 10332	A half-open range of nonnegative integers is empty iff the upper bound is not positive. (Contributed by AV, 2-May-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (0..^(𝑁 − 𝑀)) = ∅))
Theorem	fzonlt0 10333	A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑀 < 𝑁 ↔ (𝑀..^𝑁) = ∅))
Theorem	fzo0 10334	Half-open sets with equal endpoints are empty. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐴..^𝐴) = ∅
Theorem	fzonnsub 10335	If 𝐾 < 𝑁 then 𝑁 − 𝐾 is a positive integer. (Contributed by Mario Carneiro, 29-Sep-2015.) (Revised by Mario Carneiro, 1-Jan-2017.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝐾) ∈ ℕ)
Theorem	fzonnsub2 10336	If 𝑀 < 𝑁 then 𝑁 − 𝑀 is a positive integer. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝑀) ∈ ℕ)
Theorem	fzoss1 10337	Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾..^𝑁) ⊆ (𝑀..^𝑁))
Theorem	fzoss2 10338	Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀..^𝐾) ⊆ (𝑀..^𝑁))
Theorem	fzossrbm1 10339	Subset of a half open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.)
⊢ (𝑁 ∈ ℤ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
Theorem	fzo0ss1 10340	Subset relationship for half-open integer ranges with lower bounds 0 and 1. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
⊢ (1..^𝑁) ⊆ (0..^𝑁)
Theorem	fzossnn0 10341	A half-open integer range starting at a nonnegative integer is a subset of the nonnegative integers. (Contributed by Alexander van der Vekens, 13-May-2018.)
⊢ (𝑀 ∈ ℕ0 → (𝑀..^𝑁) ⊆ ℕ0)
Theorem	fzospliti 10342	One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 ∈ (𝐵..^𝐷) ∨ 𝐴 ∈ (𝐷..^𝐶)))
Theorem	fzosplit 10343	Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ (𝐷 ∈ (𝐵...𝐶) → (𝐵..^𝐶) = ((𝐵..^𝐷) ∪ (𝐷..^𝐶)))
Theorem	fzodisj 10344	Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015.)
⊢ ((𝐴..^𝐵) ∩ (𝐵..^𝐶)) = ∅
Theorem	fzouzsplit 10345	Split an upper integer set into a half-open integer range and another upper integer set. (Contributed by Mario Carneiro, 21-Sep-2016.)
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (ℤ≥‘𝐴) = ((𝐴..^𝐵) ∪ (ℤ≥‘𝐵)))
Theorem	fzouzdisj 10346	A half-open integer range does not overlap the upper integer range starting at the endpoint of the first range. (Contributed by Mario Carneiro, 21-Sep-2016.)
⊢ ((𝐴..^𝐵) ∩ (ℤ≥‘𝐵)) = ∅
Theorem	fzoun 10347	A half-open integer range as union of two half-open integer ranges. (Contributed by AV, 23-Apr-2022.)
⊢ ((𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐶 ∈ ℕ0) → (𝐴..^(𝐵 + 𝐶)) = ((𝐴..^𝐵) ∪ (𝐵..^(𝐵 + 𝐶))))
Theorem	fzodisjsn 10348	A half-open integer range and the singleton of its upper bound are disjoint. (Contributed by AV, 7-Mar-2021.)
⊢ ((𝐴..^𝐵) ∩ {𝐵}) = ∅
Theorem	lbfzo0 10349	An integer is strictly greater than zero iff it is a member of ℕ. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ (0 ∈ (0..^𝐴) ↔ 𝐴 ∈ ℕ)
Theorem	elfzo0 10350	Membership in a half-open integer range based at 0. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵))
Theorem	fzo1fzo0n0 10351	An integer between 1 and an upper bound of a half-open integer range is not 0 and between 0 and the upper bound of the half-open integer range. (Contributed by Alexander van der Vekens, 21-Mar-2018.)
⊢ (𝐾 ∈ (1..^𝑁) ↔ (𝐾 ∈ (0..^𝑁) ∧ 𝐾 ≠ 0))
Theorem	elfzo0z 10352	Membership in a half-open range of nonnegative integers, generalization of elfzo0 10350 requiring the upper bound to be an integer only. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵))
Theorem	elfzo0le 10353	A member in a half-open range of nonnegative integers is less than or equal to the upper bound of the range. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 ≤ 𝐵)
Theorem	elfzonn0 10354	A member of a half-open range of nonnegative integers is a nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
⊢ (𝐾 ∈ (0..^𝑁) → 𝐾 ∈ ℕ0)
Theorem	fzonmapblen 10355	The result of subtracting a nonnegative integer from a positive integer and adding another nonnegative integer which is less than the first one is less then the positive integer. (Contributed by Alexander van der Vekens, 19-May-2018.)
⊢ ((𝐴 ∈ (0..^𝑁) ∧ 𝐵 ∈ (0..^𝑁) ∧ 𝐵 < 𝐴) → (𝐵 + (𝑁 − 𝐴)) < 𝑁)
Theorem	fzofzim 10356	If a nonnegative integer in a finite interval of integers is not the upper bound of the interval, it is contained in the corresponding half-open integer range. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
⊢ ((𝐾 ≠ 𝑀 ∧ 𝐾 ∈ (0...𝑀)) → 𝐾 ∈ (0..^𝑀))
Theorem	fzossnn 10357	Half-open integer ranges starting with 1 are subsets of ℕ. (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ (1..^𝑁) ⊆ ℕ
Theorem	elfzo1 10358	Membership in a half-open integer range based at 1. (Contributed by Thierry Arnoux, 14-Feb-2017.)
⊢ (𝑁 ∈ (1..^𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀))
Theorem	fzo0m 10359*	A half-open integer range based at 0 is inhabited precisely if the upper bound is a positive integer. (Contributed by Jim Kingdon, 20-Apr-2020.)
⊢ (∃𝑥 𝑥 ∈ (0..^𝐴) ↔ 𝐴 ∈ ℕ)
Theorem	fzoaddel 10360	Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ ((𝐵 + 𝐷)..^(𝐶 + 𝐷)))
Theorem	fzo0addel 10361	Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020.)
⊢ ((𝐴 ∈ (0..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ (𝐷..^(𝐶 + 𝐷)))
Theorem	fzo0addelr 10362	Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020.)
⊢ ((𝐴 ∈ (0..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ (𝐷..^(𝐷 + 𝐶)))
Theorem	fzoaddel2 10363	Translate membership in a shifted-down half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐴 ∈ (0..^(𝐵 − 𝐶)) ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 + 𝐶) ∈ (𝐶..^𝐵))
Theorem	elfzoextl 10364	Membership of an integer in an extended open range of integers, extension added to the left. (Contributed by AV, 31-Aug-2025.) Generalized by replacing the left border of the ranges. (Revised by SN, 18-Sep-2025.)
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑍 ∈ (𝑀..^(𝐼 + 𝑁)))
Theorem	elfzoext 10365	Membership of an integer in an extended open range of integers, extension added to the right. (Contributed by AV, 30-Apr-2020.) (Proof shortened by AV, 23-Sep-2025.)
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑍 ∈ (𝑀..^(𝑁 + 𝐼)))
Theorem	elincfzoext 10366	Membership of an increased integer in a correspondingly extended half-open range of integers. (Contributed by AV, 30-Apr-2020.)
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → (𝑍 + 𝐼) ∈ (𝑀..^(𝑁 + 𝐼)))
Theorem	fzosubel 10367	Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 − 𝐷) ∈ ((𝐵 − 𝐷)..^(𝐶 − 𝐷)))
Theorem	fzosubel2 10368	Membership in a translated half-open integer range implies translated membership in the original range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐴 ∈ ((𝐵 + 𝐶)..^(𝐵 + 𝐷)) ∧ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (𝐴 − 𝐵) ∈ (𝐶..^𝐷))
Theorem	fzosubel3 10369	Membership in a translated half-open integer range when the original range is zero-based. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝐴 ∈ (𝐵..^(𝐵 + 𝐷)) ∧ 𝐷 ∈ ℤ) → (𝐴 − 𝐵) ∈ (0..^𝐷))
Theorem	eluzgtdifelfzo 10370	Membership of the difference of integers in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑁 ∈ (ℤ≥‘𝐴) ∧ 𝐵 < 𝐴) → (𝑁 − 𝐴) ∈ (0..^(𝑁 − 𝐵))))
Theorem	ige2m2fzo 10371	Membership of an integer greater than 1 decreased by 2 in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (𝑁 − 2) ∈ (0..^(𝑁 − 1)))
Theorem	fzocatel 10372	Translate membership in a half-open integer range. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (((𝐴 ∈ (0..^(𝐵 + 𝐶)) ∧ ¬ 𝐴 ∈ (0..^𝐵)) ∧ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ)) → (𝐴 − 𝐵) ∈ (0..^𝐶))
Theorem	ubmelfzo 10373	If an integer in a 1 based finite set of sequential integers is subtracted from the upper bound of this finite set of sequential integers, the result is contained in a half-open range of nonnegative integers with the same upper bound. (Contributed by AV, 18-Mar-2018.) (Revised by AV, 30-Oct-2018.)
⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − 𝐾) ∈ (0..^𝑁))
Theorem	elfzodifsumelfzo 10374	If an integer is in a half-open range of nonnegative integers with a difference as upper bound, the sum of the integer with the subtrahend of the difference is in the a half-open range of nonnegative integers containing the minuend of the difference. (Contributed by AV, 13-Nov-2018.)
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...𝑃)) → (𝐼 ∈ (0..^(𝑁 − 𝑀)) → (𝐼 + 𝑀) ∈ (0..^𝑃)))
Theorem	elfzom1elp1fzo 10375	Membership of an integer incremented by one in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Proof shortened by AV, 5-Jan-2020.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(𝑁 − 1))) → (𝐼 + 1) ∈ (0..^𝑁))
Theorem	elfzom1elfzo 10376	Membership in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 18-Jun-2018.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(𝑁 − 1))) → 𝐼 ∈ (0..^𝑁))
Theorem	fzval3 10377	Expressing a closed integer range as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝑁 ∈ ℤ → (𝑀...𝑁) = (𝑀..^(𝑁 + 1)))
Theorem	fzosn 10378	Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ (𝐴 ∈ ℤ → (𝐴..^(𝐴 + 1)) = {𝐴})
Theorem	elfzomin 10379	Membership of an integer in the smallest open range of integers. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ (𝑍 ∈ ℤ → 𝑍 ∈ (𝑍..^(𝑍 + 1)))
Theorem	zpnn0elfzo 10380	Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑍 + 𝑁) ∈ (𝑍..^((𝑍 + 𝑁) + 1)))
Theorem	zpnn0elfzo1 10381	Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝑍 + 𝑁) ∈ (𝑍..^(𝑍 + (𝑁 + 1))))
Theorem	fzosplitsnm1 10382	Removing a singleton from a half-open integer range at the end. (Contributed by Alexander van der Vekens, 23-Mar-2018.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (ℤ≥‘(𝐴 + 1))) → (𝐴..^𝐵) = ((𝐴..^(𝐵 − 1)) ∪ {(𝐵 − 1)}))
Theorem	elfzonlteqm1 10383	If an element of a half-open integer range is not less than the upper bound of the range decreased by 1, it must be equal to the upper bound of the range decreased by 1. (Contributed by AV, 3-Nov-2018.)
⊢ ((𝐴 ∈ (0..^𝐵) ∧ ¬ 𝐴 < (𝐵 − 1)) → 𝐴 = (𝐵 − 1))
Theorem	fzonn0p1 10384	A nonnegative integer is element of the half-open range of nonnegative integers with the element increased by one as an upper bound. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0..^(𝑁 + 1)))
Theorem	fzossfzop1 10385	A half-open range of nonnegative integers is a subset of a half-open range of nonnegative integers with the upper bound increased by one. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
⊢ (𝑁 ∈ ℕ0 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
Theorem	fzonn0p1p1 10386	If a nonnegative integer is element of a half-open range of nonnegative integers, increasing this integer by one results in an element of a half- open range of nonnegative integers with the upper bound increased by one. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
⊢ (𝐼 ∈ (0..^𝑁) → (𝐼 + 1) ∈ (0..^(𝑁 + 1)))
Theorem	elfzom1p1elfzo 10387	Increasing an element of a half-open range of nonnegative integers by 1 results in an element of the half-open range of nonnegative integers with an upper bound increased by 1. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ (0..^(𝑁 − 1))) → (𝑋 + 1) ∈ (0..^𝑁))
Theorem	fzo0ssnn0 10388	Half-open integer ranges starting with 0 are subsets of NN0. (Contributed by Thierry Arnoux, 8-Oct-2018.)
⊢ (0..^𝑁) ⊆ ℕ0
Theorem	fzo01 10389	Expressing the singleton of 0 as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (0..^1) = {0}
Theorem	fzo12sn 10390	A 1-based half-open integer interval up to, but not including, 2 is a singleton. (Contributed by Alexander van der Vekens, 31-Jan-2018.)
⊢ (1..^2) = {1}
Theorem	fzo0to2pr 10391	A half-open integer range from 0 to 2 is an unordered pair. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (0..^2) = {0, 1}
Theorem	fzo0to3tp 10392	A half-open integer range from 0 to 3 is an unordered triple. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
⊢ (0..^3) = {0, 1, 2}
Theorem	fzo0to42pr 10393	A half-open integer range from 0 to 4 is a union of two unordered pairs. (Contributed by Alexander van der Vekens, 17-Nov-2017.)
⊢ (0..^4) = ({0, 1} ∪ {2, 3})
Theorem	fzo0sn0fzo1 10394	A half-open range of nonnegative integers is the union of the singleton set containing 0 and a half-open range of positive integers. (Contributed by Alexander van der Vekens, 18-May-2018.)
⊢ (𝑁 ∈ ℕ → (0..^𝑁) = ({0} ∪ (1..^𝑁)))
Theorem	fzoend 10395	The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐴 ∈ (𝐴..^𝐵) → (𝐵 − 1) ∈ (𝐴..^𝐵))
Theorem	fzo0end 10396	The endpoint of a zero-based half-open range. (Contributed by Stefan O'Rear, 27-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
⊢ (𝐵 ∈ ℕ → (𝐵 − 1) ∈ (0..^𝐵))
Theorem	ssfzo12 10397	Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))
Theorem	ssfzo12bi 10398	Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 5-Nov-2018.)
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))
Theorem	ubmelm1fzo 10399	The result of subtracting 1 and an integer of a half-open range of nonnegative integers from the upper bound of this range is contained in this range. (Contributed by AV, 23-Mar-2018.) (Revised by AV, 30-Oct-2018.)
⊢ (𝐾 ∈ (0..^𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁))
Theorem	fzofzp1 10400	If a point is in a half-open range, the next point is in the closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ (𝐴...𝐵))