Type  Label  Description 
Statement 

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

..^


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

..^ 

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

..^ 

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

..^ 

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

..^ 

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

..^


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

..^ 

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

..^ 

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

..^ 

Theorem  fzolb 9110 
The left endpoint of a halfopen integer interval is in the set iff the
two arguments are integers with . This
provides an alternative
notation for the "strict upper integer" predicate by analogy to
the "weak
upper integer" predicate .
(Contributed by Mario
Carneiro, 29Sep2015.)

..^ 

Theorem  fzolb2 9111 
The left endpoint of a halfopen integer interval is in the set iff the
two arguments are integers with . This
provides an alternative
notation for the "strict upper integer" predicate by analogy to
the "weak
upper integer" predicate .
(Contributed by Mario
Carneiro, 29Sep2015.)

..^


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

..^ 

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

..^ 

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

..^ 

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

..^ ..^ 

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

..^ ..^ 

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

..^ 

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

..^ 

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

..^ 

Theorem  elfzo3 9120 
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 9121* 
A halfopen integer interval is inhabited iff it contains its left
endpoint. (Contributed by Jim Kingdon, 20Apr2020.)

..^ ..^ 

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

..^ 

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

..^ 

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

..^


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

..^ 

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

..^ 

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

..^ 

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

..^ ..^ 

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

..^ ..^ 

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

..^ ..^ 

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

..^ ..^ 

Theorem  fzossnn0 9132 
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 9133 
One direction of splitting a halfopen integer range in half.
(Contributed by Stefan O'Rear, 14Aug2015.)

..^
..^ ..^ 

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

..^ ..^ ..^ 

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

..^ ..^


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

..^ 

Theorem  fzouzdisj 9137 
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 9138 
An integer is strictly greater than zero iff it is a member of .
(Contributed by Mario Carneiro, 29Sep2015.)

..^


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

..^ 

Theorem  fzo1fzo0n0 9140 
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 9141 
Membership in a halfopen range of nonnegative integers, generalization of
elfzo0 9139 requiring the upper bound to be an integer
only. (Contributed by
Alexander van der Vekens, 23Sep2018.)

..^ 

Theorem  elfzo0le 9142 
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 9143 
A member of a halfopen range of nonnegative integers is a nonnegative
integer. (Contributed by Alexander van der Vekens, 21May2018.)

..^


Theorem  fzonmapblen 9144 
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 9145 
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 9146 
Halfopen integer ranges starting with 1 are subsets of NN. (Contributed
by Thierry Arnoux, 28Dec2016.)

..^ 

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

..^ 

Theorem  fzo0m 9148* 
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 9149 
Translate membership in a halfopen integer range. (Contributed by Stefan
O'Rear, 15Aug2015.)

..^
..^


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

..^
..^ 

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

..^
..^ 

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

..^
..^ 

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

..^
..^ 

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

..^ 

Theorem  ige2m2fzo 9155 
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 9156 
Translate membership in a halfopen integer range. (Contributed by
Thierry Arnoux, 28Sep2018.)

..^ ..^
..^ 

Theorem  ubmelfzo 9157 
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 9158 
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 9159 
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 9160 
Membership in a halfopen range of nonnegative integers. (Contributed by
Alexander van der Vekens, 18Jun2018.)

..^
..^ 

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

..^


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

..^ 

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

..^ 

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

..^


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

..^


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

..^ ..^ 

Theorem  elfzonlteqm1 9167 
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 9168 
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 9169 
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 9170 
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 9171 
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 9172 
Halfopen integer ranges starting with 0 are subsets of NN0.
(Contributed by Thierry Arnoux, 8Oct2018.)

..^ 

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

..^ 

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

..^ 

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

..^ 

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

..^ 

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

..^ 

Theorem  fzo0sn0fzo1 9178 
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 9179 
The endpoint of a halfopen integer range. (Contributed by Mario
Carneiro, 29Sep2015.)

..^ ..^ 

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

..^ 

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

..^ ..^ 

Theorem  ssfzo12bi 9182 
Subset relationship for halfopen integer ranges. (Contributed by
Alexander van der Vekens, 5Nov2018.)

..^ ..^


Theorem  ubmelm1fzo 9183 
The result of subtracting 1 and an integer of a halfopen range of
nonnegative integers from the upper bound of this range is contained in
this range. (Contributed by AV, 23Mar2018.) (Revised by AV,
30Oct2018.)

..^
..^ 

Theorem  fzofzp1 9184 
If a point is in a halfopen range, the next point is in the closed range.
(Contributed by Stefan O'Rear, 23Aug2015.)

..^


Theorem  fzofzp1b 9185 
If a point is in a halfopen range, the next point is in the closed range.
(Contributed by Mario Carneiro, 27Sep2015.)

..^


Theorem  elfzom1b 9186 
An integer is a member of a 1based finite set of sequential integers iff
its predecessor is a member of the corresponding 0based set.
(Contributed by Mario Carneiro, 27Sep2015.)

..^
..^ 

Theorem  elfzonelfzo 9187 
If an element of a halfopen integer range is not contained in the lower
subrange, it must be in the upper subrange. (Contributed by Alexander van
der Vekens, 30Mar2018.)

..^ ..^
..^ 

Theorem  elfzomelpfzo 9188 
An integer increased by another integer is an element of a halfopen
integer range if and only if the integer is contained in the halfopen
integer range with bounds decreased by the other integer. (Contributed by
Alexander van der Vekens, 30Mar2018.)

..^
..^ 

Theorem  peano2fzor 9189 
A Peanopostulatelike theorem for downward closure of a halfopen integer
range. (Contributed by Mario Carneiro, 1Oct2015.)

..^
..^ 

Theorem  fzosplitsn 9190 
Extending a halfopen range by a singleton on the end. (Contributed by
Stefan O'Rear, 23Aug2015.)

..^ ..^ 

Theorem  fzosplitprm1 9191 
Extending a halfopen integer range by an unordered pair at the end.
(Contributed by Alexander van der Vekens, 22Sep2018.)

..^ ..^ 

Theorem  fzosplitsni 9192 
Membership in a halfopen range extended by a singleton. (Contributed by
Stefan O'Rear, 23Aug2015.)

..^ ..^ 

Theorem  fzisfzounsn 9193 
A finite interval of integers as union of a halfopen integer range and a
singleton. (Contributed by Alexander van der Vekens, 15Jun2018.)

..^ 

Theorem  fzostep1 9194 
Two possibilities for a number one greater than a number in a halfopen
range. (Contributed by Stefan O'Rear, 23Aug2015.)

..^ ..^


Theorem  fzoshftral 9195* 
Shift the scanning order inside of a quantification over a halfopen
integer range, analogous to fzshftral 9071. (Contributed by Alexander van
der Vekens, 23Sep2018.)

..^ ..^ 

Theorem  fzind2 9196* 
Induction on the integers from to
inclusive. The first four
hypotheses give us the substitution instances we need; the last two are
the basis and the induction step. Version of fzind 8411 using integer
range definitions. (Contributed by Mario Carneiro, 6Feb2016.)

..^ 

Theorem  fvinim0ffz 9197 
The function values for the borders of a finite interval of integers,
which is the domain of the function, are not in the image of the
interior of the interval iff the intersection of the images of the
interior and the borders is empty. (Contributed by Alexander van der
Vekens, 31Oct2017.) (Revised by AV, 5Feb2021.)

..^
..^ ..^ 

Theorem  subfzo0 9198 
The difference between two elements in a halfopen range of nonnegative
integers is greater than the negation of the upper bound and less than the
upper bound of the range. (Contributed by AV, 20Mar2021.)

..^ ..^


3.5.7 Rational numbers (cont.)


Theorem  qtri3or 9199 
Rational trichotomy. (Contributed by Jim Kingdon, 6Oct2021.)



Theorem  qletric 9200 
Rational trichotomy. (Contributed by Jim Kingdon, 6Oct2021.)

