Home | Metamath
Proof Explorer Theorem List (p. 131 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elfz0ubfz0 13001 | 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 13002 | 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 13003 | 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 13004 | 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 13005 | 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 13006 | 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 13007 | 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 13008 | 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 13009 | 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 13010 | 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 13011 | 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 13012 | Express the set of nonnegative integers as the disjoint (see nn0disj 13013) union of the first 𝑁 + 1 values and the rest. (Contributed by AV, 8-Nov-2019.) |
⊢ (𝑁 ∈ ℕ0 → ℕ0 = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) | ||
Theorem | nn0disj 13013 | 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 | fz0sn0fz1 13014 | A finite set of sequential nonnegative integers is the union of the singleton containing 0 and a finite set of sequential positive integers. (Contributed by AV, 20-Mar-2021.) |
⊢ (𝑁 ∈ ℕ0 → (0...𝑁) = ({0} ∪ (1...𝑁))) | ||
Theorem | fvffz0 13015 | The function value of a function from a finite interval of nonnegative integers. (Contributed by AV, 13-Feb-2021.) |
⊢ (((𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁) ∧ 𝑃:(0...𝑁)⟶𝑉) → (𝑃‘𝐼) ∈ 𝑉) | ||
Theorem | 1fv 13016 | A function on a singleton. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Proof shortened by AV, 18-Apr-2021.) |
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑃 = {〈0, 𝑁〉}) → (𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁)) | ||
Theorem | 4fvwrd4 13017* | 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 13018* | 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...𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) | ||
Theorem | preduz 13019 | The value of the predecessor class over an upper integer set. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → Pred( < , (ℤ≥‘𝑀), 𝑁) = (𝑀...(𝑁 − 1))) | ||
Theorem | prednn 13020 | The value of the predecessor class over the naturals. (Contributed by Scott Fenton, 6-Aug-2013.) |
⊢ (𝑁 ∈ ℕ → Pred( < , ℕ, 𝑁) = (1...(𝑁 − 1))) | ||
Theorem | prednn0 13021 | The value of the predecessor class over ℕ0. (Contributed by Scott Fenton, 9-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → Pred( < , ℕ0, 𝑁) = (0...(𝑁 − 1))) | ||
Theorem | predfz 13022 | Calculate the predecessor of an integer under a finite set of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → Pred( < , (𝑀...𝑁), 𝐾) = (𝑀...(𝐾 − 1))) | ||
Syntax | cfzo 13023 | Syntax for half-open integer ranges. |
class ..^ | ||
Definition | df-fzo 13024* | 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 12883, which includes 𝑁. Not including the endpoint simplifies a number of formulas related to cardinality and splitting; contrast fzosplit 13060 with fzsplit 12923, for instance. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1))) | ||
Theorem | fzof 13025 | Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ | ||
Theorem | elfzoel1 13026 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ) | ||
Theorem | elfzoel2 13027 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ) | ||
Theorem | elfzoelz 13028 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ) | ||
Theorem | fzoval 13029 | 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 13030 | Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) | ||
Theorem | elfzo2 13031 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁)) | ||
Theorem | elfzouz 13032 | Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) | ||
Theorem | nelfzo 13033 | An integer not being a member of a half-open finite set of integers. (Contributed by AV, 29-Apr-2020.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∉ (𝑀..^𝑁) ↔ (𝐾 < 𝑀 ∨ 𝑁 ≤ 𝐾))) | ||
Theorem | fzolb 13034 | 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 13035 | 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 13036 | 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 13037 | A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 < 𝑁) | ||
Theorem | elfzolt3 13038 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 < 𝑁) | ||
Theorem | elfzolt2b 13039 | A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝐾..^𝑁)) | ||
Theorem | elfzolt3b 13040 | Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝑀 ∈ (𝑀..^𝑁)) | ||
Theorem | fzonel 13041 | A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ ¬ 𝐵 ∈ (𝐴..^𝐵) | ||
Theorem | elfzouz2 13042 | 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 13043 | A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ∈ (𝑀...𝑁)) | ||
Theorem | elfzo3 13044 | 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 13045 | A half-open integer interval is nonempty iff it contains its left endpoint. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ ((𝑀..^𝑁) ≠ ∅ ↔ 𝑀 ∈ (𝑀..^𝑁)) | ||
Theorem | fzossfz 13046 | 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 13047 | A half-open integer interval is a set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑀..^𝑁) ⊆ ℤ | ||
Theorem | fzon 13048 | 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 13049 | 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 13050 | A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑀 < 𝑁 ↔ (𝑀..^𝑁) = ∅)) | ||
Theorem | fzo0 13051 | 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 13052 | If 𝐾 < 𝑁 then 𝑁 − 𝐾 is a positive integer. (Contributed by Mario Carneiro, 29-Sep-2015.) (Revised by Mario Carneiro, 1-Jan-2017.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝐾) ∈ ℕ) | ||
Theorem | fzonnsub2 13053 | If 𝑀 < 𝑁 then 𝑁 − 𝑀 is a positive integer. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝑁 − 𝑀) ∈ ℕ) | ||
Theorem | fzoss1 13054 | 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 13055 | 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 13056 | Subset of a half-open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
⊢ (𝑁 ∈ ℤ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) | ||
Theorem | fzo0ss1 13057 | 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 13058 | 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 13059 | One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 ∈ (𝐵..^𝐷) ∨ 𝐴 ∈ (𝐷..^𝐶))) | ||
Theorem | fzosplit 13060 | Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐷 ∈ (𝐵...𝐶) → (𝐵..^𝐶) = ((𝐵..^𝐷) ∪ (𝐷..^𝐶))) | ||
Theorem | fzodisj 13061 | Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ((𝐴..^𝐵) ∩ (𝐵..^𝐶)) = ∅ | ||
Theorem | fzouzsplit 13062 | 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 13063 | 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 13064 | A half-open integer range as union of two half-open integer ranges. (Contributed by AV, 23-Apr-2022.) |
⊢ ((𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐶 ∈ ℕ0) → (𝐴..^(𝐵 + 𝐶)) = ((𝐴..^𝐵) ∪ (𝐵..^(𝐵 + 𝐶)))) | ||
Theorem | fzodisjsn 13065 | A half-open integer range and the singleton of its upper bound are disjoint. (Contributed by AV, 7-Mar-2021.) |
⊢ ((𝐴..^𝐵) ∩ {𝐵}) = ∅ | ||
Theorem | prinfzo0 13066 | 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 13067 | An integer is strictly greater than zero iff it is a member of ℕ. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (0 ∈ (0..^𝐴) ↔ 𝐴 ∈ ℕ) | ||
Theorem | elfzo0 13068 | 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 13069 | Membership in a half-open range of nonnegative integers, generalization of elfzo0 13068 requiring the upper bound to be an integer only. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵)) | ||
Theorem | nn0p1elfzo 13070 | 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 13071 | 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 13072 | 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 13073 | 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 13074 | 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 13075 | Translation of one between closed and open integer ranges. (Contributed by Thierry Arnoux, 28-Jul-2020.) |
⊢ (𝑀 ∈ (1...𝑁) → (𝑀 − 1) ∈ (0..^𝑁)) | ||
Theorem | fzossnn 13076 | Half-open integer ranges starting with 1 are subsets of NN. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
⊢ (1..^𝑁) ⊆ ℕ | ||
Theorem | elfzo1 13077 | Membership in a half-open integer range based at 1. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝑁 ∈ (1..^𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀)) | ||
Theorem | fzo1fzo0n0 13078 | 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 13079 | 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 13080 | Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ ((𝐵 + 𝐷)..^(𝐶 + 𝐷))) | ||
Theorem | fzo0addel 13081 | Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020.) |
⊢ ((𝐴 ∈ (0..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ (𝐷..^(𝐶 + 𝐷))) | ||
Theorem | fzo0addelr 13082 | Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020.) |
⊢ ((𝐴 ∈ (0..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 + 𝐷) ∈ (𝐷..^(𝐷 + 𝐶))) | ||
Theorem | fzoaddel2 13083 | Translate membership in a shifted-down half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐴 ∈ (0..^(𝐵 − 𝐶)) ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 + 𝐶) ∈ (𝐶..^𝐵)) | ||
Theorem | elfzoext 13084 | Membership of an integer in an extended open range of integers. (Contributed by AV, 30-Apr-2020.) |
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → 𝑍 ∈ (𝑀..^(𝑁 + 𝐼))) | ||
Theorem | elincfzoext 13085 | Membership of an increased integer in a correspondingly extended half-open range of integers. (Contributed by AV, 30-Apr-2020.) |
⊢ ((𝑍 ∈ (𝑀..^𝑁) ∧ 𝐼 ∈ ℕ0) → (𝑍 + 𝐼) ∈ (𝑀..^(𝑁 + 𝐼))) | ||
Theorem | fzosubel 13086 | Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐴 ∈ (𝐵..^𝐶) ∧ 𝐷 ∈ ℤ) → (𝐴 − 𝐷) ∈ ((𝐵 − 𝐷)..^(𝐶 − 𝐷))) | ||
Theorem | fzosubel2 13087 | 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 13088 | 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 13089 | 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 13090 | 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 13091 | Translate membership in a half-open integer range. (Contributed by Thierry Arnoux, 28-Sep-2018.) |
⊢ (((𝐴 ∈ (0..^(𝐵 + 𝐶)) ∧ ¬ 𝐴 ∈ (0..^𝐵)) ∧ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ)) → (𝐴 − 𝐵) ∈ (0..^𝐶)) | ||
Theorem | ubmelfzo 13092 | 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 13093 | 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 13094 | 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 13095 | Membership in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 18-Jun-2018.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(𝑁 − 1))) → 𝐼 ∈ (0..^𝑁)) | ||
Theorem | fzval3 13096 | Expressing a closed integer range as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝑁 ∈ ℤ → (𝑀...𝑁) = (𝑀..^(𝑁 + 1))) | ||
Theorem | fz0add1fz1 13097 | 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 13098 | Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (𝐴 ∈ ℤ → (𝐴..^(𝐴 + 1)) = {𝐴}) | ||
Theorem | elfzomin 13099 | Membership of an integer in the smallest open range of integers. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ (𝑍 ∈ ℤ → 𝑍 ∈ (𝑍..^(𝑍 + 1))) | ||
Theorem | zpnn0elfzo 13100 | 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))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |