Type  Label  Description 
Statement 

Theorem  elfz0ubfz0 9501 
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, 3Apr2018.)



Theorem  elfz0fzfz0 9502 
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,
27May2018.)



Theorem  fz0fzelfz0 9503 
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, 21Apr2018.)



Theorem  fznn0sub2 9504 
Subtraction closure for a member of a finite set of sequential nonnegative
integers. (Contributed by NM, 26Sep2005.) (Revised by Mario Carneiro,
28Apr2015.)



Theorem  uzsubfz0 9505 
Membership of an integer greater than L decreased by L in a finite set of
sequential nonnegative integers. (Contributed by Alexander van der
Vekens, 16Sep2018.)



Theorem  fz0fzdiffz0 9506 
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, 6Jun2018.)



Theorem  elfzmlbm 9507 
Subtracting the lower bound of a finite set of sequential integers from an
element of this set. (Contributed by Alexander van der Vekens,
29Mar2018.) (Proof shortened by OpenAI, 25Mar2020.)



Theorem  elfzmlbp 9508 
Subtracting the lower bound of a finite set of sequential integers from an
element of this set. (Contributed by Alexander van der Vekens,
29Mar2018.)



Theorem  fzctr 9509 
Lemma for theorems about the central binomial coefficient. (Contributed
by Mario Carneiro, 8Mar2014.) (Revised by Mario Carneiro,
2Aug2014.)



Theorem  difelfzle 9510 
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, 12Jun2018.)



Theorem  difelfznle 9511 
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,
12Jun2018.)



Theorem  nn0split 9512 
Express the set of nonnegative integers as the disjoint (see nn0disj 9514)
union of the first values and the rest.
(Contributed by AV,
8Nov2019.)



Theorem  nnsplit 9513 
Express the set of positive integers as the disjoint union of the first
values and the
rest. (Contributed by Glauco Siliprandi,
21Nov2020.)



Theorem  nn0disj 9514 
The first elements of the set of nonnegative integers are
distinct from any later members. (Contributed by AV, 8Nov2019.)



Theorem  1fv 9515 
A one value function. (Contributed by Alexander van der Vekens,
3Dec2017.)



Theorem  4fvwrd4 9516* 
The first four function values of a word of length at least 4.
(Contributed by Alexander van der Vekens, 18Nov2017.)



Theorem  2ffzeq 9517* 
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, 30Jun2018.)



3.5.6 Halfopen integer ranges


Syntax  cfzo 9518 
Syntax for halfopen integer ranges.

..^ 

Definition  dffzo 9519* 
Define a function generating sets of integers using a halfopen range.
Read ..^ as the integers from up to, but not
including, ;
contrast with dffz 9394, which
includes . Not
including the endpoint simplifies a number of
formulas related to cardinality and splitting; contrast fzosplit 9553 with
fzsplit 9434, for instance. (Contributed by Stefan
O'Rear,
14Aug2015.)

..^


Theorem  fzof 9520 
Functionality of the halfopen integer set function. (Contributed by
Stefan O'Rear, 14Aug2015.)

..^ 

Theorem  elfzoel1 9521 
Reverse closure for halfopen integer sets. (Contributed by Stefan
O'Rear, 14Aug2015.)

..^ 

Theorem  elfzoel2 9522 
Reverse closure for halfopen integer sets. (Contributed by Stefan
O'Rear, 14Aug2015.)

..^ 

Theorem  elfzoelz 9523 
Reverse closure for halfopen integer sets. (Contributed by Stefan
O'Rear, 14Aug2015.)

..^ 

Theorem  fzoval 9524 
Value of the halfopen integer set in terms of the closed integer set.
(Contributed by Stefan O'Rear, 14Aug2015.)

..^


Theorem  elfzo 9525 
Membership in a halfopen finite set of integers. (Contributed by Stefan
O'Rear, 15Aug2015.)

..^ 

Theorem  elfzo2 9526 
Membership in a halfopen integer interval. (Contributed by Mario
Carneiro, 29Sep2015.)

..^ 

Theorem  elfzouz 9527 
Membership in a halfopen integer interval. (Contributed by Mario
Carneiro, 29Sep2015.)

..^ 

Theorem  fzodcel 9528 
Decidability of membership in a halfopen integer interval. (Contributed
by Jim Kingdon, 25Aug2022.)

DECID ..^ 

Theorem  fzolb 9529 
The left endpoint of a halfopen 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, 29Sep2015.)

..^ 

Theorem  fzolb2 9530 
The left endpoint of a halfopen 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, 29Sep2015.)

..^


Theorem  elfzole1 9531 
A member in a halfopen integer interval is greater than or equal to the
lower bound. (Contributed by Stefan O'Rear, 15Aug2015.)

..^ 

Theorem  elfzolt2 9532 
A member in a halfopen integer interval is less than the upper bound.
(Contributed by Stefan O'Rear, 15Aug2015.)

..^ 

Theorem  elfzolt3 9533 
Membership in a halfopen integer interval implies that the bounds are
unequal. (Contributed by Stefan O'Rear, 15Aug2015.)

..^ 

Theorem  elfzolt2b 9534 
A member in a halfopen integer interval is less than the upper bound.
(Contributed by Mario Carneiro, 29Sep2015.)

..^ ..^ 

Theorem  elfzolt3b 9535 
Membership in a halfopen integer interval implies that the bounds are
unequal. (Contributed by Mario Carneiro, 29Sep2015.)

..^ ..^ 

Theorem  fzonel 9536 
A halfopen range does not contain its right endpoint. (Contributed by
Stefan O'Rear, 25Aug2015.)

..^ 

Theorem  elfzouz2 9537 
The upper bound of a halfopen range is greater or equal to an element of
the range. (Contributed by Mario Carneiro, 29Sep2015.)

..^ 

Theorem  elfzofz 9538 
A halfopen range is contained in the corresponding closed range.
(Contributed by Stefan O'Rear, 23Aug2015.)

..^ 

Theorem  elfzo3 9539 
Express membership in a halfopen integer interval in terms of the "less
than or equal" and "less than" predicates on integers,
resp.
, ..^
.
(Contributed by Mario Carneiro, 29Sep2015.)

..^ ..^ 

Theorem  fzom 9540* 
A halfopen integer interval is inhabited iff it contains its left
endpoint. (Contributed by Jim Kingdon, 20Apr2020.)

..^ ..^ 

Theorem  fzossfz 9541 
A halfopen range is contained in the corresponding closed range.
(Contributed by Stefan O'Rear, 23Aug2015.) (Revised by Mario
Carneiro, 29Sep2015.)

..^ 

Theorem  fzon 9542 
A halfopen set of sequential integers is empty if the bounds are equal or
reversed. (Contributed by Alexander van der Vekens, 30Oct2017.)

..^ 

Theorem  fzonlt0 9543 
A halfopen integer range is empty if the bounds are equal or reversed.
(Contributed by AV, 20Oct2018.)

..^


Theorem  fzo0 9544 
Halfopen sets with equal endpoints are empty. (Contributed by Stefan
O'Rear, 15Aug2015.) (Revised by Mario Carneiro, 29Sep2015.)

..^ 

Theorem  fzonnsub 9545 
If then is a positive integer.
(Contributed by Mario
Carneiro, 29Sep2015.) (Revised by Mario Carneiro, 1Jan2017.)

..^ 

Theorem  fzonnsub2 9546 
If then is a positive integer.
(Contributed by Mario
Carneiro, 1Jan2017.)

..^ 

Theorem  fzoss1 9547 
Subset relationship for halfopen sequences of integers. (Contributed
by Stefan O'Rear, 15Aug2015.) (Revised by Mario Carneiro,
29Sep2015.)

..^ ..^ 

Theorem  fzoss2 9548 
Subset relationship for halfopen sequences of integers. (Contributed by
Stefan O'Rear, 15Aug2015.) (Revised by Mario Carneiro, 29Sep2015.)

..^ ..^ 

Theorem  fzossrbm1 9549 
Subset of a half open range. (Contributed by Alexander van der Vekens,
1Nov2017.)

..^ ..^ 

Theorem  fzo0ss1 9550 
Subset relationship for halfopen integer ranges with lower bounds 0 and
1. (Contributed by Alexander van der Vekens, 18Mar2018.)

..^ ..^ 

Theorem  fzossnn0 9551 
A halfopen integer range starting at a nonnegative integer is a subset of
the nonnegative integers. (Contributed by Alexander van der Vekens,
13May2018.)

..^ 

Theorem  fzospliti 9552 
One direction of splitting a halfopen integer range in half.
(Contributed by Stefan O'Rear, 14Aug2015.)

..^
..^ ..^ 

Theorem  fzosplit 9553 
Split a halfopen integer range in half. (Contributed by Stefan O'Rear,
14Aug2015.)

..^ ..^ ..^ 

Theorem  fzodisj 9554 
Abutting halfopen integer ranges are disjoint. (Contributed by Stefan
O'Rear, 14Aug2015.)

..^ ..^


Theorem  fzouzsplit 9555 
Split an upper integer set into a halfopen integer range and another
upper integer set. (Contributed by Mario Carneiro, 21Sep2016.)

..^ 

Theorem  fzouzdisj 9556 
A halfopen integer range does not overlap the upper integer range
starting at the endpoint of the first range. (Contributed by Mario
Carneiro, 21Sep2016.)

..^


Theorem  lbfzo0 9557 
An integer is strictly greater than zero iff it is a member of .
(Contributed by Mario Carneiro, 29Sep2015.)

..^


Theorem  elfzo0 9558 
Membership in a halfopen integer range based at 0. (Contributed by
Stefan O'Rear, 15Aug2015.) (Revised by Mario Carneiro, 29Sep2015.)

..^ 

Theorem  fzo1fzo0n0 9559 
An integer between 1 and an upper bound of a halfopen integer range is
not 0 and between 0 and the upper bound of the halfopen integer range.
(Contributed by Alexander van der Vekens, 21Mar2018.)

..^ ..^ 

Theorem  elfzo0z 9560 
Membership in a halfopen range of nonnegative integers, generalization of
elfzo0 9558 requiring the upper bound to be an integer
only. (Contributed by
Alexander van der Vekens, 23Sep2018.)

..^ 

Theorem  elfzo0le 9561 
A member in a halfopen range of nonnegative integers is less than or
equal to the upper bound of the range. (Contributed by Alexander van der
Vekens, 23Sep2018.)

..^ 

Theorem  elfzonn0 9562 
A member of a halfopen range of nonnegative integers is a nonnegative
integer. (Contributed by Alexander van der Vekens, 21May2018.)

..^


Theorem  fzonmapblen 9563 
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,
19May2018.)

..^
..^


Theorem  fzofzim 9564 
If a nonnegative integer in a finite interval of integers is not the upper
bound of the interval, it is contained in the corresponding halfopen
integer range. (Contributed by Alexander van der Vekens, 15Jun2018.)

..^ 

Theorem  fzossnn 9565 
Halfopen integer ranges starting with 1 are subsets of NN. (Contributed
by Thierry Arnoux, 28Dec2016.)

..^ 

Theorem  elfzo1 9566 
Membership in a halfopen integer range based at 1. (Contributed by
Thierry Arnoux, 14Feb2017.)

..^ 

Theorem  fzo0m 9567* 
A halfopen integer range based at 0 is inhabited precisely if the upper
bound is a positive integer. (Contributed by Jim Kingdon,
20Apr2020.)

..^ 

Theorem  fzoaddel 9568 
Translate membership in a halfopen integer range. (Contributed by Stefan
O'Rear, 15Aug2015.)

..^
..^


Theorem  fzoaddel2 9569 
Translate membership in a shifteddown halfopen integer range.
(Contributed by Stefan O'Rear, 15Aug2015.)

..^
..^ 

Theorem  fzosubel 9570 
Translate membership in a halfopen integer range. (Contributed by Stefan
O'Rear, 15Aug2015.)

..^
..^ 

Theorem  fzosubel2 9571 
Membership in a translated halfopen integer range implies translated
membership in the original range. (Contributed by Stefan O'Rear,
15Aug2015.)

..^
..^ 

Theorem  fzosubel3 9572 
Membership in a translated halfopen integer range when the original range
is zerobased. (Contributed by Stefan O'Rear, 15Aug2015.)

..^
..^ 

Theorem  eluzgtdifelfzo 9573 
Membership of the difference of integers in a halfopen range of
nonnegative integers. (Contributed by Alexander van der Vekens,
17Sep2018.)

..^ 

Theorem  ige2m2fzo 9574 
Membership of an integer greater than 1 decreased by 2 in a halfopen
range of nonnegative integers. (Contributed by Alexander van der Vekens,
3Oct2018.)

..^ 

Theorem  fzocatel 9575 
Translate membership in a halfopen integer range. (Contributed by
Thierry Arnoux, 28Sep2018.)

..^ ..^
..^ 

Theorem  ubmelfzo 9576 
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 halfopen range of nonnegative integers with the same
upper bound. (Contributed by AV, 18Mar2018.) (Revised by AV,
30Oct2018.)

..^ 

Theorem  elfzodifsumelfzo 9577 
If an integer is in a halfopen 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 halfopen range of nonnegative integers
containing the minuend of the difference. (Contributed by AV,
13Nov2018.)

..^
..^ 

Theorem  elfzom1elp1fzo 9578 
Membership of an integer incremented by one in a halfopen range of
nonnegative integers. (Contributed by Alexander van der Vekens,
24Jun2018.) (Proof shortened by AV, 5Jan2020.)

..^ ..^ 

Theorem  elfzom1elfzo 9579 
Membership in a halfopen range of nonnegative integers. (Contributed by
Alexander van der Vekens, 18Jun2018.)

..^
..^ 

Theorem  fzval3 9580 
Expressing a closed integer range as a halfopen integer range.
(Contributed by Stefan O'Rear, 15Aug2015.)

..^


Theorem  fzosn 9581 
Expressing a singleton as a halfopen range. (Contributed by Stefan
O'Rear, 23Aug2015.)

..^ 

Theorem  elfzomin 9582 
Membership of an integer in the smallest open range of integers.
(Contributed by Alexander van der Vekens, 22Sep2018.)

..^ 

Theorem  zpnn0elfzo 9583 
Membership of an integer increased by a nonnegative integer in a half
open integer range. (Contributed by Alexander van der Vekens,
22Sep2018.)

..^


Theorem  zpnn0elfzo1 9584 
Membership of an integer increased by a nonnegative integer in a half
open integer range. (Contributed by Alexander van der Vekens,
22Sep2018.)

..^


Theorem  fzosplitsnm1 9585 
Removing a singleton from a halfopen integer range at the end.
(Contributed by Alexander van der Vekens, 23Mar2018.)

..^ ..^ 

Theorem  elfzonlteqm1 9586 
If an element of a halfopen 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, 3Nov2018.)

..^ 

Theorem  fzonn0p1 9587 
A nonnegative integer is element of the halfopen range of nonnegative
integers with the element increased by one as an upper bound.
(Contributed by Alexander van der Vekens, 5Aug2018.)

..^


Theorem  fzossfzop1 9588 
A halfopen range of nonnegative integers is a subset of a halfopen range
of nonnegative integers with the upper bound increased by one.
(Contributed by Alexander van der Vekens, 5Aug2018.)

..^ ..^ 

Theorem  fzonn0p1p1 9589 
If a nonnegative integer is element of a halfopen 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, 5Aug2018.)

..^
..^ 

Theorem  elfzom1p1elfzo 9590 
Increasing an element of a halfopen range of nonnegative integers by 1
results in an element of the halfopen range of nonnegative integers with
an upper bound increased by 1. (Contributed by Alexander van der Vekens,
1Aug2018.)

..^ ..^ 

Theorem  fzo0ssnn0 9591 
Halfopen integer ranges starting with 0 are subsets of NN0.
(Contributed by Thierry Arnoux, 8Oct2018.)

..^ 

Theorem  fzo01 9592 
Expressing the singleton of as a halfopen integer range.
(Contributed by Stefan O'Rear, 15Aug2015.)

..^ 

Theorem  fzo12sn 9593 
A 1based halfopen integer interval up to, but not including, 2 is a
singleton. (Contributed by Alexander van der Vekens, 31Jan2018.)

..^ 

Theorem  fzo0to2pr 9594 
A halfopen integer range from 0 to 2 is an unordered pair. (Contributed
by Alexander van der Vekens, 4Dec2017.)

..^ 

Theorem  fzo0to3tp 9595 
A halfopen integer range from 0 to 3 is an unordered triple.
(Contributed by Alexander van der Vekens, 9Nov2017.)

..^ 

Theorem  fzo0to42pr 9596 
A halfopen integer range from 0 to 4 is a union of two unordered pairs.
(Contributed by Alexander van der Vekens, 17Nov2017.)

..^ 

Theorem  fzo0sn0fzo1 9597 
A halfopen range of nonnegative integers is the union of the singleton
set containing 0 and a halfopen range of positive integers. (Contributed
by Alexander van der Vekens, 18May2018.)

..^ ..^ 

Theorem  fzoend 9598 
The endpoint of a halfopen integer range. (Contributed by Mario
Carneiro, 29Sep2015.)

..^ ..^ 

Theorem  fzo0end 9599 
The endpoint of a zerobased halfopen range. (Contributed by Stefan
O'Rear, 27Aug2015.) (Revised by Mario Carneiro, 29Sep2015.)

..^ 

Theorem  ssfzo12 9600 
Subset relationship for halfopen integer ranges. (Contributed by
Alexander van der Vekens, 16Mar2018.)

..^ ..^ 