| Metamath
Proof Explorer Theorem List (p. 138 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | elfzo 13701 | Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) | ||
| Theorem | elfzo2 13702 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁)) | ||
| Theorem | elfzouz 13703 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) | ||
| Theorem | nelfzo 13704 | An integer not being a member of a half-open finite set of integers. (Contributed by AV, 29-Apr-2020.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∉ (𝑀..^𝑁) ↔ (𝐾 < 𝑀 ∨ 𝑁 ≤ 𝐾))) | ||
| Theorem | fzolb 13705 | The left endpoint of a half-open 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, 29-Sep-2015.) |
| ⊢ (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)) | ||
| Theorem | fzolb2 13706 | The left endpoint of a half-open 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, 29-Sep-2015.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (𝑀..^𝑁) ↔ 𝑀 < 𝑁)) | ||
| Theorem | elfzole1 13707 | 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 13708 | A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 < 𝑁) | ||
| Theorem | elfzolt3 13709 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 < 𝑁) | ||
| Theorem | elfzolt2b 13710 | A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝐾..^𝑁)) | ||
| Theorem | elfzolt3b 13711 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 ∈ (𝑀..^𝑁)) | ||
| Theorem | elfzop1le2 13712 | A member in a half-open integer interval plus 1 is less than or equal to the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝐾 + 1) ≤ 𝑁) | ||
| Theorem | fzonel 13713 | A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
| ⊢ ¬ 𝐵 ∈ (𝐴..^𝐵) | ||
| Theorem | elfzouz2 13714 | The upper bound of a half-open range is greater than or equal to an element of the range. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) | ||
| Theorem | elfzofz 13715 | A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝑀...𝑁)) | ||
| Theorem | elfzo3 13716 | Express membership in a half-open integer interval in terms of the "less than or equal to" and "less than" predicates on integers, resp. 𝐾 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝐾, 𝐾 ∈ (𝐾..^𝑁) ↔ 𝐾 < 𝑁. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ (𝐾..^𝑁))) | ||
| Theorem | fzon0 13717 | A half-open integer interval is nonempty iff it contains its left endpoint. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ⊢ ((𝑀..^𝑁) ≠ ∅ ↔ 𝑀 ∈ (𝑀..^𝑁)) | ||
| Theorem | fzossfz 13718 | 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 | fzossz 13719 | A half-open integer interval is a set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝑀..^𝑁) ⊆ ℤ | ||
| Theorem | fzon 13720 | 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 13721 | 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 13722 | A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑀 < 𝑁 ↔ (𝑀..^𝑁) = ∅)) | ||
| Theorem | fzo0 13723 | 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 13724 | If 𝐾 < 𝑁 then 𝑁 − 𝐾 is a positive integer. (Contributed by Mario Carneiro, 29-Sep-2015.) (Revised by Mario Carneiro, 1-Jan-2017.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝐾) ∈ ℕ) | ||
| Theorem | fzonnsub2 13725 | If 𝑀 < 𝑁 then 𝑁 − 𝑀 is a positive integer. (Contributed by Mario Carneiro, 1-Jan-2017.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝑀) ∈ ℕ) | ||
| Theorem | fzoss1 13726 | 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 13727 | 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 13728 | Subset of a half-open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
| ⊢ (𝑁 ∈ ℤ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) | ||
| Theorem | fzo0ss1 13729 | 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 13730 | 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 13731 | One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
| ⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 ∈ (𝐵..^𝐷) ∨ 𝐴 ∈ (𝐷..^𝐶))) | ||
| Theorem | fzosplit 13732 | Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
| ⊢ (𝐷 ∈ (𝐵...𝐶) → (𝐵..^𝐶) = ((𝐵..^𝐷) ∪ (𝐷..^𝐶))) | ||
| Theorem | fzodisj 13733 | Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
| ⊢ ((𝐴..^𝐵) ∩ (𝐵..^𝐶)) = ∅ | ||
| Theorem | fzouzsplit 13734 | 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 13735 | 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 13736 | A half-open integer range as union of two half-open integer ranges. (Contributed by AV, 23-Apr-2022.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐶 ∈ ℕ0) → (𝐴..^(𝐵 + 𝐶)) = ((𝐴..^𝐵) ∪ (𝐵..^(𝐵 + 𝐶)))) | ||
| Theorem | fzodisjsn 13737 | A half-open integer range and the singleton of its upper bound are disjoint. (Contributed by AV, 7-Mar-2021.) |
| ⊢ ((𝐴..^𝐵) ∩ {𝐵}) = ∅ | ||
| Theorem | prinfzo0 13738 | The intersection of a half-open integer range and the pair of its outer left borders is empty. (Contributed by AV, 9-Jan-2021.) |
| ⊢ (𝑀 ∈ ℤ → ({𝑀, 𝑁} ∩ ((𝑀 + 1)..^𝑁)) = ∅) | ||
| Theorem | lbfzo0 13739 | An integer is strictly greater than zero iff it is a member of ℕ. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ⊢ (0 ∈ (0..^𝐴) ↔ 𝐴 ∈ ℕ) | ||
| Theorem | elfzo0 13740 | 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 | elfzo0z 13741 | Membership in a half-open range of nonnegative integers, generalization of elfzo0 13740 requiring the upper bound to be an integer only. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
| ⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵)) | ||
| Theorem | nn0p1elfzo 13742 | A nonnegative integer increased by 1 which is less than or equal to another integer is an element of a half-open range of integers. (Contributed by AV, 27-Feb-2021.) |
| ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ (𝐾 + 1) ≤ 𝑁) → 𝐾 ∈ (0..^𝑁)) | ||
| Theorem | elfzo0le 13743 | 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 | elfzolem1 13744 | A member in a half-open integer interval is less than or equal to the upper bound minus 1 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ≤ (𝑁 − 1)) | ||
| Theorem | elfzo0subge1 13745 | The difference of the upper bound of a half-open range of nonnegative integers and an element of this range is greater than or equal to 1. (Contributed by AV, 1-Sep-2025.) (Proof shortened by SN, 18-Sep-2025.) |
| ⊢ (𝐴 ∈ (0..^𝐵) → 1 ≤ (𝐵 − 𝐴)) | ||
| Theorem | elfzo0suble 13746 | The difference of the upper bound of a half-open range of nonnegative integers and an element of this range is less than or equal to the upper bound. (Contributed by AV, 1-Sep-2025.) (Proof shortened by SN, 18-Sep-2025.) |
| ⊢ (𝐴 ∈ (0..^𝐵) → (𝐵 − 𝐴) ≤ 𝐵) | ||
| Theorem | elfzonn0 13747 | 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 13748 | 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 than the positive integer. (Contributed by Alexander van der Vekens, 19-May-2018.) |
| ⊢ ((𝐴 ∈ (0..^𝑁) ∧ 𝐵 ∈ (0..^𝑁) ∧ 𝐵 < 𝐴) → (𝐵 + (𝑁 − 𝐴)) < 𝑁) | ||
| Theorem | fzofzim 13749 | 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 | fz1fzo0m1 13750 | Translation of one between closed and open integer ranges. (Contributed by Thierry Arnoux, 28-Jul-2020.) |
| ⊢ (𝑀 ∈ (1...𝑁) → (𝑀 − 1) ∈ (0..^𝑁)) | ||
| Theorem | fzossnn 13751 | Half-open integer ranges starting with 1 are subsets of ℕ. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
| ⊢ (1..^𝑁) ⊆ ℕ | ||
| Theorem | elfzo1 13752 | Membership in a half-open integer range based at 1. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
| ⊢ (𝑁 ∈ (1..^𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀)) | ||
| Theorem | fzo1lb 13753 | 1 is the left endpoint of a half-open integer range based at 1 iff the right endpoint is an integer greater than 1. (Contributed by AV, 4-Sep-2025.) |
| ⊢ (1 ∈ (1..^𝑁) ↔ 𝑁 ∈ (ℤ≥‘2)) | ||
| Theorem | fzo1fzo0n0 13754 | 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 | fzo0n0 13755 | A half-open integer range based at 0 is nonempty precisely if the upper bound is a positive integer. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
| ⊢ ((0..^𝐴) ≠ ∅ ↔ 𝐴 ∈ ℕ) | ||
| Theorem | fzoaddel 13756 | Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ ((𝐵 + 𝐷)..^(𝐶 + 𝐷))) | ||
| Theorem | fzo0addel 13757 | Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020.) |
| ⊢ ((𝐴 ∈ (0..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ (𝐷..^(𝐶 + 𝐷))) | ||
| Theorem | fzo0addelr 13758 | Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020.) |
| ⊢ ((𝐴 ∈ (0..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ (𝐷..^(𝐷 + 𝐶))) | ||
| Theorem | fzoaddel2 13759 | Translate membership in a shifted-down half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ ((𝐴 ∈ (0..^(𝐵 − 𝐶)) ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 + 𝐶) ∈ (𝐶..^𝐵)) | ||
| Theorem | elfzoextl 13760 | 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 13761 | 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 13762 | Membership of an increased integer in a correspondingly extended half-open range of integers. (Contributed by AV, 30-Apr-2020.) |
| ⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → (𝑍 + 𝐼) ∈ (𝑀..^(𝑁 + 𝐼))) | ||
| Theorem | fzosubel 13763 | Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 − 𝐷) ∈ ((𝐵 − 𝐷)..^(𝐶 − 𝐷))) | ||
| Theorem | fzosubel2 13764 | 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 13765 | 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 13766 | 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 13767 | 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 13768 | Translate membership in a half-open integer range. (Contributed by Thierry Arnoux, 28-Sep-2018.) |
| ⊢ (((𝐴 ∈ (0..^(𝐵 + 𝐶)) ∧ ¬ 𝐴 ∈ (0..^𝐵)) ∧ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ)) → (𝐴 − 𝐵) ∈ (0..^𝐶)) | ||
| Theorem | ubmelfzo 13769 | 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 13770 | 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 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 13771 | 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 13772 | Membership in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 18-Jun-2018.) |
| ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(𝑁 − 1))) → 𝐼 ∈ (0..^𝑁)) | ||
| Theorem | fzval3 13773 | Expressing a closed integer range as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ (𝑁 ∈ ℤ → (𝑀...𝑁) = (𝑀..^(𝑁 + 1))) | ||
| Theorem | fz0add1fz1 13774 | Translate membership in a 0-based half-open integer range into membership in a 1-based finite sequence of integers. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ (0..^𝑁)) → (𝑋 + 1) ∈ (1...𝑁)) | ||
| Theorem | fzosn 13775 | Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
| ⊢ (𝐴 ∈ ℤ → (𝐴..^(𝐴 + 1)) = {𝐴}) | ||
| Theorem | elfzomin 13776 | Membership of an integer in the smallest open range of integers. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
| ⊢ (𝑍 ∈ ℤ → 𝑍 ∈ (𝑍..^(𝑍 + 1))) | ||
| Theorem | zpnn0elfzo 13777 | 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 13778 | 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 13779 | 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 13780 | 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 13781 | 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 13782 | 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 13783 | 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 13784 | 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.) (Proof shortened by Thierry Arnoux, 14-Dec-2023.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ (0..^(𝑁 − 1))) → (𝑋 + 1) ∈ (0..^𝑁)) | ||
| Theorem | fzo0ssnn0 13785 | Half-open integer ranges starting with 0 are subsets of NN0. (Contributed by Thierry Arnoux, 8-Oct-2018.) (Proof shortened by JJ, 1-Jun-2021.) |
| ⊢ (0..^𝑁) ⊆ ℕ0 | ||
| Theorem | fzo01 13786 | Expressing the singleton of 0 as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ (0..^1) = {0} | ||
| Theorem | fzo12sn 13787 | 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 | fzo13pr 13788 | A 1-based half-open integer interval up to, but not including, 3 is a pair. (Contributed by Thierry Arnoux, 11-Jul-2020.) |
| ⊢ (1..^3) = {1, 2} | ||
| Theorem | fzo0to2pr 13789 | 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 | fz01pr 13790 | An integer range between 0 and 1 is a pair. (Contributed by AV, 11-Sep-2025.) |
| ⊢ (0...1) = {0, 1} | ||
| Theorem | fzo0to3tp 13791 | 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 13792 | 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 | fzo1to4tp 13793 | A half-open integer range from 1 to 4 is an unordered triple. (Contributed by AV, 28-Jul-2021.) |
| ⊢ (1..^4) = {1, 2, 3} | ||
| Theorem | fzo0sn0fzo1 13794 | 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 | elfzo0l 13795 | A member of a half-open range of nonnegative integers is either 0 or a member of the corresponding half-open range of positive integers. (Contributed by AV, 5-Feb-2021.) |
| ⊢ (𝐾 ∈ (0..^𝑁) → (𝐾 = 0 ∨ 𝐾 ∈ (1..^𝑁))) | ||
| Theorem | fzoend 13796 | The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015.) |
| ⊢ (𝐴 ∈ (𝐴..^𝐵) → (𝐵 − 1) ∈ (𝐴..^𝐵)) | ||
| Theorem | fzo0end 13797 | 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 13798 | Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | ||
| Theorem | ssfzoulel 13799 | If a half-open integer range is a subset of a half-open range of nonnegative integers, but its lower bound is greater than or equal to the upper bound of the containing range, or its upper bound is less than or equal to 0, then its upper bound is less than or equal to its lower bound (and therefore it is actually empty). (Contributed by Alexander van der Vekens, 24-May-2018.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑁 ≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝐴..^𝐵) ⊆ (0..^𝑁) → 𝐵 ≤ 𝐴))) | ||
| Theorem | ssfzo12bi 13800 | Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 5-Nov-2018.) |
| ⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |