HomeTheorem List (p. 104 of 162)
Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 104 of 162) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | elfzolt2b 10301 | A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015.) |
     ..^   ..^ | ||
| Theorem | elfzolt3b 10302 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ..^ ..^ | ||
| Theorem | fzonel 10303 | A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
   ..^ | ||
| Theorem | elfzouz2 10304 | 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 10305 | A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
..^  | ||
| Theorem | elfzo3 10306 |
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.)
|
..^ ![/\](wedge.gif "/\"){kind=small} ..^ | ||
| Theorem | fzom 10307* | A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.) |
  ..^ ..^ | ||
| Theorem | fzossfz 10308 | 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 10309 | 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 10310 | A half-open range of nonnegative integers is empty iff the upper bound is not positive. (Contributed by AV, 2-May-2020.) |
 ..^  | ||
| Theorem | fzonlt0 10311 | A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018.) |
| ..^
| ||
| Theorem | fzo0 10312 | 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 10313 |
If then is a positive integer.
(Contributed by Mario
Carneiro, 29-Sep-2015.) (Revised by Mario Carneiro, 1-Jan-2017.)
|
..^  | ||
| Theorem | fzonnsub2 10314 |
If then is a positive integer.
(Contributed by Mario
Carneiro, 1-Jan-2017.)
|
| ..^ | ||
| Theorem | fzoss1 10315 | 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 10316 | 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 10317 | Subset of a half open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
..^  ..^ | ||
| Theorem | fzo0ss1 10318 | Subset relationship for half-open integer ranges with lower bounds 0 and 1. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
| ..^ ..^ | ||
| Theorem | fzossnn0 10319 | 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.) |
 ..^ | ||
| Theorem | fzospliti 10320 | One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ 
..^  ..^ | ||
| Theorem | fzosplit 10321 | Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^ ..^  ..^ | ||
| Theorem | fzodisj 10322 | Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
..^  ..^
| ||
| Theorem | fzouzsplit 10323 | 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 10324 | 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 10325 | A half-open integer range as union of two half-open integer ranges. (Contributed by AV, 23-Apr-2022.) |
..^  ..^ ..^ | ||
| Theorem | fzodisjsn 10326 | A half-open integer range and the singleton of its upper bound are disjoint. (Contributed by AV, 7-Mar-2021.) |
..^   | ||
| Theorem | lbfzo0 10327 |
An integer is strictly greater than zero iff it is a member of .
(Contributed by Mario Carneiro, 29-Sep-2015.)
|
| ..^
| ||
| Theorem | elfzo0 10328 | 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.) |
| ..^ | ||
| Theorem | fzo1fzo0n0 10329 | 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.) |
..^ ..^  | ||
| Theorem | elfzo0z 10330 | Membership in a half-open range of nonnegative integers, generalization of elfzo0 10328 requiring the upper bound to be an integer only. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
| ..^ | ||
| Theorem | elfzo0le 10331 | 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.) |
| ..^ | ||
| Theorem | elfzonn0 10332 | A member of a half-open range of nonnegative integers is a nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.) |
| ..^
| ||
| Theorem | fzonmapblen 10333 | 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.) |
| ..^
..^
| ||
| Theorem | fzofzim 10334 | 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.) |
| ..^ | ||
| Theorem | fzossnn 10335 |
Half-open integer ranges starting with 1 are subsets of .
(Contributed by Thierry Arnoux, 28-Dec-2016.)
|
| ..^ | ||
| Theorem | elfzo1 10336 | Membership in a half-open integer range based at 1. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
| ..^ | ||
| Theorem | fzo0m 10337* | 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.) |
| ..^ | ||
| Theorem | fzoaddel 10338 | Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ..^
..^
| ||
| Theorem | fzo0addel 10339 | Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020.) |
| ..^
..^
| ||
| Theorem | fzo0addelr 10340 | Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020.) |
| ..^
..^
| ||
| Theorem | fzoaddel2 10341 | Translate membership in a shifted-down half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ..^
..^ | ||
| Theorem | elfzoextl 10342 | 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.) |
 ..^ 
..^
| ||
| Theorem | elfzoext 10343 | 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.) |
| ..^
..^
| ||
| Theorem | elincfzoext 10344 | Membership of an increased integer in a correspondingly extended half-open range of integers. (Contributed by AV, 30-Apr-2020.) |
| ..^
..^ | ||
| Theorem | fzosubel 10345 | Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ..^
..^ | ||
| Theorem | fzosubel2 10346 | 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 10347 | Membership in a translated half-open integer range when the original range is zero-based. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ..^
..^ | ||
| Theorem | eluzgtdifelfzo 10348 | Membership of the difference of integers in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
|
..^ | ||
| Theorem | ige2m2fzo 10349 | 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.) |
..^ | ||
| Theorem | fzocatel 10350 | Translate membership in a half-open integer range. (Contributed by Thierry Arnoux, 28-Sep-2018.) |
| ..^ ..^
..^ | ||
| Theorem | ubmelfzo 10351 | 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.) |
|
..^ | ||
| Theorem | elfzodifsumelfzo 10352 | 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.) |
 ..^
..^ | ||
| Theorem | elfzom1elp1fzo 10353 | 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.) |
| ..^ ..^ | ||
| Theorem | elfzom1elfzo 10354 | Membership in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 18-Jun-2018.) |
| ..^
..^ | ||
| Theorem | fzval3 10355 | Expressing a closed integer range as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
|
..^
| ||
| Theorem | fzosn 10356 | Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
| ..^ | ||
| Theorem | elfzomin 10357 | Membership of an integer in the smallest open range of integers. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
| ..^ | ||
| Theorem | zpnn0elfzo 10358 | Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
|
..^
| ||
| Theorem | zpnn0elfzo1 10359 | Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
|
..^
| ||
| Theorem | fzosplitsnm1 10360 | Removing a singleton from a half-open integer range at the end. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
| ..^ ..^ | ||
| Theorem | elfzonlteqm1 10361 | 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.) |
| ..^ | ||
| Theorem | fzonn0p1 10362 | 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.) |
|
..^
| ||
| Theorem | fzossfzop1 10363 | 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.) |
| ..^ ..^ | ||
| Theorem | fzonn0p1p1 10364 | 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.) |
| ..^
..^ | ||
| Theorem | elfzom1p1elfzo 10365 | 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.) |
 ..^ ..^ | ||
| Theorem | fzo0ssnn0 10366 | Half-open integer ranges starting with 0 are subsets of NN0. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
| ..^ | ||
| Theorem | fzo01 10367 |
Expressing the singleton of as a half-open integer range.
(Contributed by Stefan O'Rear, 15-Aug-2015.)
|
| ..^ | ||
| Theorem | fzo12sn 10368 | 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.) |
| ..^ | ||
| Theorem | fzo0to2pr 10369 | A half-open integer range from 0 to 2 is an unordered pair. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
..^  | ||
| Theorem | fzo0to3tp 10370 | A half-open integer range from 0 to 3 is an unordered triple. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
..^ | ||
| Theorem | fzo0to42pr 10371 | 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.) |
..^ | ||
| Theorem | fzo0sn0fzo1 10372 | 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.) |
| ..^ ..^ | ||
| Theorem | fzoend 10373 | The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ..^ ..^ | ||
| Theorem | fzo0end 10374 | The endpoint of a zero-based half-open range. (Contributed by Stefan O'Rear, 27-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
| ..^ | ||
| Theorem | ssfzo12 10375 | Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
 ..^ ..^ | ||
| Theorem | ssfzo12bi 10376 | Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 5-Nov-2018.) |
|
..^ ..^
| ||
| Theorem | ubmelm1fzo 10377 | 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.) |
| ..^
..^ | ||
| Theorem | fzofzp1 10378 | 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.) |
| ..^
| ||
| Theorem | fzofzp1b 10379 | If a point is in a half-open range, the next point is in the closed range. (Contributed by Mario Carneiro, 27-Sep-2015.) |
|
..^
| ||
| Theorem | elfzom1b 10380 | An integer is a member of a 1-based finite set of sequential integers iff its predecessor is a member of the corresponding 0-based set. (Contributed by Mario Carneiro, 27-Sep-2015.) |
| ..^
..^ | ||
| Theorem | elfzonelfzo 10381 | If an element of a half-open integer range is not contained in the lower subrange, it must be in the upper subrange. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
..^ ..^
..^ | ||
| Theorem | elfzomelpfzo 10382 | An integer increased by another integer is an element of a half-open integer range if and only if the integer is contained in the half-open integer range with bounds decreased by the other integer. (Contributed by Alexander van der Vekens, 30-Mar-2018.) |
|
..^
..^ | ||
| Theorem | peano2fzor 10383 | A Peano-postulate-like theorem for downward closure of a half-open integer range. (Contributed by Mario Carneiro, 1-Oct-2015.) |
| ..^
..^ | ||
| Theorem | fzosplitsn 10384 | Extending a half-open range by a singleton on the end. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
| ..^ ..^ | ||
| Theorem | fzosplitprm1 10385 | Extending a half-open integer range by an unordered pair at the end. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
| ..^ ..^ | ||
| Theorem | fzosplitsni 10386 | Membership in a half-open range extended by a singleton. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
|
..^ ..^ | ||
| Theorem | fzisfzounsn 10387 | A finite interval of integers as union of a half-open integer range and a singleton. (Contributed by Alexander van der Vekens, 15-Jun-2018.) |
| ..^ | ||
| Theorem | fzostep1 10388 | Two possibilities for a number one greater than a number in a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
| ..^ ..^
| ||
| Theorem | fzoshftral 10389* | Shift the scanning order inside of a quantification over a half-open integer range, analogous to fzshftral 10250. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
  ..^  ..^   ![].](_drbrack.gif "]."){kind=small} | ||
| Theorem | fzind2 10390* |
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 9508 using integer
range definitions. (Contributed by Mario Carneiro, 6-Feb-2016.)
|
 
 
..^  | ||
| Theorem | exfzdc 10391* | Decidability of the existence of an integer defined by a decidable proposition. (Contributed by Jim Kingdon, 28-Jan-2022.) |
DECID
DECID | ||
| Theorem | fvinim0ffz 10392 | 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, 31-Oct-2017.) (Revised by AV, 5-Feb-2021.) |
   
..^ 
..^ ..^ | ||
| Theorem | subfzo0 10393 | The difference between two elements in a half-open 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, 20-Mar-2021.) |
..^  ..^ 
| ||
| Theorem | zsupcllemstep 10394* | Lemma for zsupcl 10396. Induction step. (Contributed by Jim Kingdon, 7-Dec-2021.) |
DECID
 
| ||
| Theorem | zsupcllemex 10395* | Lemma for zsupcl 10396. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.) |
|
DECID
| ||
| Theorem | zsupcl 10396* |
Closure of supremum for decidable integer properties. The property
which defines the set we are taking the supremum of must (a) be true at
(which
corresponds to the nonempty condition of classical supremum
theorems), (b) decidable at each value after , and (c) be false
after (which
corresponds to the upper bound condition found in
classical supremum theorems). (Contributed by Jim Kingdon,
7-Dec-2021.)
|
DECID
| ||
| Theorem | zssinfcl 10397* | The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
|
inf inf | ||
| Theorem | infssuzex 10398* | Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.) |
DECID
| ||
| Theorem | infssuzledc 10399* | The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by Jim Kingdon, 13-Jan-2022.) |
|
DECID inf | ||
| Theorem | infssuzcldc 10400* | The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by Jim Kingdon, 20-Jan-2022.) |
|
DECID inf | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |