Theorem List for Intuitionistic Logic Explorer - 9901-10000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fz0tp 9901 |
An integer range from 0 to 2 is an unordered triple. (Contributed by
Alexander van der Vekens, 1-Feb-2018.)
|
⊢ (0...2) = {0, 1, 2} |
|
Theorem | elfz0ubfz0 9902 |
An element of a finite set of sequential nonnegative integers is an
element of a finite set of sequential nonnegative integers with the upper
bound being an element of the finite set of sequential nonnegative
integers with the same lower bound as for the first interval and the
element under consideration as upper bound. (Contributed by Alexander van
der Vekens, 3-Apr-2018.)
|
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → 𝐾 ∈ (0...𝐿)) |
|
Theorem | elfz0fzfz0 9903 |
A member of a finite set of sequential nonnegative integers is a member of
a finite set of sequential nonnegative integers with a member of a finite
set of sequential nonnegative integers starting at the upper bound of the
first interval. (Contributed by Alexander van der Vekens,
27-May-2018.)
|
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → 𝑀 ∈ (0...𝑁)) |
|
Theorem | fz0fzelfz0 9904 |
If a member of a finite set of sequential integers with a lower bound
being a member of a finite set of sequential nonnegative integers with the
same upper bound, this member is also a member of the finite set of
sequential nonnegative integers. (Contributed by Alexander van der
Vekens, 21-Apr-2018.)
|
⊢ ((𝑁 ∈ (0...𝑅) ∧ 𝑀 ∈ (𝑁...𝑅)) → 𝑀 ∈ (0...𝑅)) |
|
Theorem | fznn0sub2 9905 |
Subtraction closure for a member of a finite set of sequential nonnegative
integers. (Contributed by NM, 26-Sep-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈ (0...𝑁)) |
|
Theorem | uzsubfz0 9906 |
Membership of an integer greater than L decreased by L in a finite set of
sequential nonnegative integers. (Contributed by Alexander van der
Vekens, 16-Sep-2018.)
|
⊢ ((𝐿 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝐿)) → (𝑁 − 𝐿) ∈ (0...𝑁)) |
|
Theorem | fz0fzdiffz0 9907 |
The difference of an integer in a finite set of sequential nonnegative
integers and and an integer of a finite set of sequential integers with
the same upper bound and the nonnegative integer as lower bound is a
member of the finite set of sequential nonnegative integers. (Contributed
by Alexander van der Vekens, 6-Jun-2018.)
|
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐾 − 𝑀) ∈ (0...𝑁)) |
|
Theorem | elfzmlbm 9908 |
Subtracting the lower bound of a finite set of sequential integers from an
element of this set. (Contributed by Alexander van der Vekens,
29-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
|
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝐾 − 𝑀) ∈ (0...(𝑁 − 𝑀))) |
|
Theorem | elfzmlbp 9909 |
Subtracting the lower bound of a finite set of sequential integers from an
element of this set. (Contributed by Alexander van der Vekens,
29-Mar-2018.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ (𝑀...(𝑀 + 𝑁))) → (𝐾 − 𝑀) ∈ (0...𝑁)) |
|
Theorem | fzctr 9910 |
Lemma for theorems about the central binomial coefficient. (Contributed
by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro,
2-Aug-2014.)
|
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0...(2 · 𝑁))) |
|
Theorem | difelfzle 9911 |
The difference of two integers from a finite set of sequential nonnegative
integers is also element of this finite set of sequential integers.
(Contributed by Alexander van der Vekens, 12-Jun-2018.)
|
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝑀 ∈ (0...𝑁) ∧ 𝐾 ≤ 𝑀) → (𝑀 − 𝐾) ∈ (0...𝑁)) |
|
Theorem | difelfznle 9912 |
The difference of two integers from a finite set of sequential nonnegative
integers increased by the upper bound is also element of this finite set
of sequential integers. (Contributed by Alexander van der Vekens,
12-Jun-2018.)
|
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝑀 ∈ (0...𝑁) ∧ ¬ 𝐾 ≤ 𝑀) → ((𝑀 + 𝑁) − 𝐾) ∈ (0...𝑁)) |
|
Theorem | nn0split 9913 |
Express the set of nonnegative integers as the disjoint (see nn0disj 9915)
union of the first 𝑁 + 1 values and the rest.
(Contributed by AV,
8-Nov-2019.)
|
⊢ (𝑁 ∈ ℕ0 →
ℕ0 = ((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))) |
|
Theorem | nnsplit 9914 |
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 9915 |
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 9916 |
A function on a singleton. (Contributed by Alexander van der Vekens,
3-Dec-2017.)
|
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑃 = {〈0, 𝑁〉}) → (𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁)) |
|
Theorem | 4fvwrd4 9917* |
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 9918* |
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 9919 |
Syntax for half-open integer ranges.
|
class ..^ |
|
Definition | df-fzo 9920* |
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 9791, which
includes 𝑁. Not including the endpoint
simplifies a number of
formulas related to cardinality and splitting; contrast fzosplit 9954 with
fzsplit 9831, for instance. (Contributed by Stefan
O'Rear,
14-Aug-2015.)
|
⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1))) |
|
Theorem | fzof 9921 |
Functionality of the half-open integer set function. (Contributed by
Stefan O'Rear, 14-Aug-2015.)
|
⊢ ..^:(ℤ ×
ℤ)⟶𝒫 ℤ |
|
Theorem | elfzoel1 9922 |
Reverse closure for half-open integer sets. (Contributed by Stefan
O'Rear, 14-Aug-2015.)
|
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ) |
|
Theorem | elfzoel2 9923 |
Reverse closure for half-open integer sets. (Contributed by Stefan
O'Rear, 14-Aug-2015.)
|
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ) |
|
Theorem | elfzoelz 9924 |
Reverse closure for half-open integer sets. (Contributed by Stefan
O'Rear, 14-Aug-2015.)
|
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ) |
|
Theorem | fzoval 9925 |
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 9926 |
Membership in a half-open finite set of integers. (Contributed by Stefan
O'Rear, 15-Aug-2015.)
|
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) |
|
Theorem | elfzo2 9927 |
Membership in a half-open integer interval. (Contributed by Mario
Carneiro, 29-Sep-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁)) |
|
Theorem | elfzouz 9928 |
Membership in a half-open integer interval. (Contributed by Mario
Carneiro, 29-Sep-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) |
|
Theorem | fzodcel 9929 |
Decidability of membership in a half-open integer interval. (Contributed
by Jim Kingdon, 25-Aug-2022.)
|
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝐾
∈ (𝑀..^𝑁)) |
|
Theorem | fzolb 9930 |
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 9931 |
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 9932 |
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 9933 |
A member in a half-open integer interval is less than the upper bound.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 < 𝑁) |
|
Theorem | elfzolt3 9934 |
Membership in a half-open integer interval implies that the bounds are
unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 < 𝑁) |
|
Theorem | elfzolt2b 9935 |
A member in a half-open integer interval is less than the upper bound.
(Contributed by Mario Carneiro, 29-Sep-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝐾..^𝑁)) |
|
Theorem | elfzolt3b 9936 |
Membership in a half-open integer interval implies that the bounds are
unequal. (Contributed by Mario Carneiro, 29-Sep-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 ∈ (𝑀..^𝑁)) |
|
Theorem | fzonel 9937 |
A half-open range does not contain its right endpoint. (Contributed by
Stefan O'Rear, 25-Aug-2015.)
|
⊢ ¬ 𝐵 ∈ (𝐴..^𝐵) |
|
Theorem | elfzouz2 9938 |
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 9939 |
A half-open range is contained in the corresponding closed range.
(Contributed by Stefan O'Rear, 23-Aug-2015.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝑀...𝑁)) |
|
Theorem | elfzo3 9940 |
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 9941* |
A half-open integer interval is inhabited iff it contains its left
endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.)
|
⊢ (∃𝑥 𝑥 ∈ (𝑀..^𝑁) ↔ 𝑀 ∈ (𝑀..^𝑁)) |
|
Theorem | fzossfz 9942 |
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 9943 |
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 | fzonlt0 9944 |
A half-open integer range is empty if the bounds are equal or reversed.
(Contributed by AV, 20-Oct-2018.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑀 < 𝑁 ↔ (𝑀..^𝑁) = ∅)) |
|
Theorem | fzo0 9945 |
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 9946 |
If 𝐾 <
𝑁 then 𝑁 − 𝐾 is a positive integer.
(Contributed by Mario
Carneiro, 29-Sep-2015.) (Revised by Mario Carneiro, 1-Jan-2017.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝐾) ∈ ℕ) |
|
Theorem | fzonnsub2 9947 |
If 𝑀 <
𝑁 then 𝑁 − 𝑀 is a positive integer.
(Contributed by Mario
Carneiro, 1-Jan-2017.)
|
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝑀) ∈ ℕ) |
|
Theorem | fzoss1 9948 |
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 9949 |
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 9950 |
Subset of a half open range. (Contributed by Alexander van der Vekens,
1-Nov-2017.)
|
⊢ (𝑁 ∈ ℤ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) |
|
Theorem | fzo0ss1 9951 |
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 9952 |
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 9953 |
One direction of splitting a half-open integer range in half.
(Contributed by Stefan O'Rear, 14-Aug-2015.)
|
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 ∈ (𝐵..^𝐷) ∨ 𝐴 ∈ (𝐷..^𝐶))) |
|
Theorem | fzosplit 9954 |
Split a half-open integer range in half. (Contributed by Stefan O'Rear,
14-Aug-2015.)
|
⊢ (𝐷 ∈ (𝐵...𝐶) → (𝐵..^𝐶) = ((𝐵..^𝐷) ∪ (𝐷..^𝐶))) |
|
Theorem | fzodisj 9955 |
Abutting half-open integer ranges are disjoint. (Contributed by Stefan
O'Rear, 14-Aug-2015.)
|
⊢ ((𝐴..^𝐵) ∩ (𝐵..^𝐶)) = ∅ |
|
Theorem | fzouzsplit 9956 |
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 9957 |
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 | lbfzo0 9958 |
An integer is strictly greater than zero iff it is a member of ℕ.
(Contributed by Mario Carneiro, 29-Sep-2015.)
|
⊢ (0 ∈ (0..^𝐴) ↔ 𝐴 ∈ ℕ) |
|
Theorem | elfzo0 9959 |
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 9960 |
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 9961 |
Membership in a half-open range of nonnegative integers, generalization of
elfzo0 9959 requiring the upper bound to be an integer
only. (Contributed by
Alexander van der Vekens, 23-Sep-2018.)
|
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵)) |
|
Theorem | elfzo0le 9962 |
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 9963 |
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 9964 |
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 9965 |
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 9966 |
Half-open integer ranges starting with 1 are subsets of NN. (Contributed
by Thierry Arnoux, 28-Dec-2016.)
|
⊢ (1..^𝑁) ⊆ ℕ |
|
Theorem | elfzo1 9967 |
Membership in a half-open integer range based at 1. (Contributed by
Thierry Arnoux, 14-Feb-2017.)
|
⊢ (𝑁 ∈ (1..^𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀)) |
|
Theorem | fzo0m 9968* |
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 9969 |
Translate membership in a half-open integer range. (Contributed by Stefan
O'Rear, 15-Aug-2015.)
|
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ ((𝐵 + 𝐷)..^(𝐶 + 𝐷))) |
|
Theorem | fzoaddel2 9970 |
Translate membership in a shifted-down half-open integer range.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ ((𝐴 ∈ (0..^(𝐵 − 𝐶)) ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 + 𝐶) ∈ (𝐶..^𝐵)) |
|
Theorem | fzosubel 9971 |
Translate membership in a half-open integer range. (Contributed by Stefan
O'Rear, 15-Aug-2015.)
|
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 − 𝐷) ∈ ((𝐵 − 𝐷)..^(𝐶 − 𝐷))) |
|
Theorem | fzosubel2 9972 |
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 9973 |
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 9974 |
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 9975 |
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 9976 |
Translate membership in a half-open integer range. (Contributed by
Thierry Arnoux, 28-Sep-2018.)
|
⊢ (((𝐴 ∈ (0..^(𝐵 + 𝐶)) ∧ ¬ 𝐴 ∈ (0..^𝐵)) ∧ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ)) → (𝐴 − 𝐵) ∈ (0..^𝐶)) |
|
Theorem | ubmelfzo 9977 |
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 9978 |
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 9979 |
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 9980 |
Membership in a half-open range of nonnegative integers. (Contributed by
Alexander van der Vekens, 18-Jun-2018.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(𝑁 − 1))) → 𝐼 ∈ (0..^𝑁)) |
|
Theorem | fzval3 9981 |
Expressing a closed integer range as a half-open integer range.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ (𝑁 ∈ ℤ → (𝑀...𝑁) = (𝑀..^(𝑁 + 1))) |
|
Theorem | fzosn 9982 |
Expressing a singleton as a half-open range. (Contributed by Stefan
O'Rear, 23-Aug-2015.)
|
⊢ (𝐴 ∈ ℤ → (𝐴..^(𝐴 + 1)) = {𝐴}) |
|
Theorem | elfzomin 9983 |
Membership of an integer in the smallest open range of integers.
(Contributed by Alexander van der Vekens, 22-Sep-2018.)
|
⊢ (𝑍 ∈ ℤ → 𝑍 ∈ (𝑍..^(𝑍 + 1))) |
|
Theorem | zpnn0elfzo 9984 |
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 9985 |
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 9986 |
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 9987 |
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 9988 |
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 9989 |
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 9990 |
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 9991 |
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 9992 |
Half-open integer ranges starting with 0 are subsets of NN0.
(Contributed by Thierry Arnoux, 8-Oct-2018.)
|
⊢ (0..^𝑁) ⊆
ℕ0 |
|
Theorem | fzo01 9993 |
Expressing the singleton of 0 as a half-open integer
range.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
⊢ (0..^1) = {0} |
|
Theorem | fzo12sn 9994 |
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 9995 |
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 9996 |
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 9997 |
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 9998 |
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 9999 |
The endpoint of a half-open integer range. (Contributed by Mario
Carneiro, 29-Sep-2015.)
|
⊢ (𝐴 ∈ (𝐴..^𝐵) → (𝐵 − 1) ∈ (𝐴..^𝐵)) |
|
Theorem | fzo0end 10000 |
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..^𝐵)) |