Home | Metamath
Proof Explorer Theorem List (p. 135 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fz1ssnn 13401 | A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (1...𝐴) ⊆ ℕ | ||
Theorem | fznn0sub 13402 | Subtraction closure for a member of a finite set of sequential integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑁 − 𝐾) ∈ ℕ0) | ||
Theorem | fzmmmeqm 13403 | Subtracting the difference of a member of a finite range of integers and the lower bound of the range from the difference of the upper bound and the lower bound of the range results in the difference of the upper bound of the range and the member. (Contributed by Alexander van der Vekens, 27-May-2018.) |
⊢ (𝑀 ∈ (𝐿...𝑁) → ((𝑁 − 𝐿) − (𝑀 − 𝐿)) = (𝑁 − 𝑀)) | ||
Theorem | fzaddel 13404 | Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) | ||
Theorem | fzadd2 13405 | Membership of a sum in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑂 ∈ ℤ ∧ 𝑃 ∈ ℤ)) → ((𝐽 ∈ (𝑀...𝑁) ∧ 𝐾 ∈ (𝑂...𝑃)) → (𝐽 + 𝐾) ∈ ((𝑀 + 𝑂)...(𝑁 + 𝑃)))) | ||
Theorem | fzsubel 13406 | Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾)))) | ||
Theorem | fzopth 13407 | A finite set of sequential integers has the ordered pair property (compare opth 5432) under certain conditions. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾))) | ||
Theorem | fzass4 13408 | Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐵 ∈ (𝐴...𝐷) ∧ 𝐶 ∈ (𝐵...𝐷)) ↔ (𝐵 ∈ (𝐴...𝐶) ∧ 𝐶 ∈ (𝐴...𝐷))) | ||
Theorem | fzss1 13409 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) | ||
Theorem | fzss2 13410 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁)) | ||
Theorem | fzssuz 13411 | A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀) | ||
Theorem | fzsn 13412 | A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) | ||
Theorem | fzssp1 13413 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1)) | ||
Theorem | fzssnn 13414 | Finite sets of sequential integers starting from a natural are a subset of the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017.) |
⊢ (𝑀 ∈ ℕ → (𝑀...𝑁) ⊆ ℕ) | ||
Theorem | ssfzunsnext 13415 | A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 13-Nov-2021.) |
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (𝑆 ∪ {𝐼}) ⊆ (if(𝐼 ≤ 𝑀, 𝐼, 𝑀)...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) | ||
Theorem | ssfzunsn 13416 | A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 8-Jun-2021.) (Proof shortened by AV, 13-Nov-2021.) |
⊢ ((𝑆 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝑆 ∪ {𝐼}) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) | ||
Theorem | fzsuc 13417 | Join a successor to the end of a finite set of sequential integers. (Contributed by NM, 19-Jul-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)})) | ||
Theorem | fzpred 13418 | Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) | ||
Theorem | fzpreddisj 13419 | A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ({𝑀} ∩ ((𝑀 + 1)...𝑁)) = ∅) | ||
Theorem | elfzp1 13420 | Append an element to a finite set of sequential integers. (Contributed by NM, 19-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1)))) | ||
Theorem | fzp1ss 13421 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) | ||
Theorem | fzelp1 13422 | Membership in a set of sequential integers with an appended element. (Contributed by NM, 7-Dec-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (𝑀...(𝑁 + 1))) | ||
Theorem | fzp1elp1 13423 | Add one to an element of a finite set of integers. (Contributed by Jeff Madsen, 6-Jun-2010.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝐾 + 1) ∈ (𝑀...(𝑁 + 1))) | ||
Theorem | fznatpl1 13424 | Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁)) | ||
Theorem | fzpr 13425 | A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)}) | ||
Theorem | fztp 13426 | A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 7-Mar-2014.) |
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 2)) = {𝑀, (𝑀 + 1), (𝑀 + 2)}) | ||
Theorem | fz12pr 13427 | An integer range between 1 and 2 is a pair. (Contributed by AV, 11-Jan-2023.) |
⊢ (1...2) = {1, 2} | ||
Theorem | fzsuc2 13428 | Join a successor to the end of a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Mar-2014.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)})) | ||
Theorem | fzp1disj 13429 | (𝑀...(𝑁 + 1)) is the disjoint union of (𝑀...𝑁) with {(𝑁 + 1)}. (Contributed by Mario Carneiro, 7-Mar-2014.) |
⊢ ((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅ | ||
Theorem | fzdifsuc 13430 | Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) | ||
Theorem | fzprval 13431* | Two ways of defining the first two values of a sequence on ℕ. (Contributed by NM, 5-Sep-2011.) |
⊢ (∀𝑥 ∈ (1...2)(𝐹‘𝑥) = if(𝑥 = 1, 𝐴, 𝐵) ↔ ((𝐹‘1) = 𝐴 ∧ (𝐹‘2) = 𝐵)) | ||
Theorem | fztpval 13432* | Two ways of defining the first three values of a sequence on ℕ. (Contributed by NM, 13-Sep-2011.) |
⊢ (∀𝑥 ∈ (1...3)(𝐹‘𝑥) = if(𝑥 = 1, 𝐴, if(𝑥 = 2, 𝐵, 𝐶)) ↔ ((𝐹‘1) = 𝐴 ∧ (𝐹‘2) = 𝐵 ∧ (𝐹‘3) = 𝐶)) | ||
Theorem | fzrev 13433 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)) ↔ (𝐽 − 𝐾) ∈ (𝑀...𝑁))) | ||
Theorem | fzrev2 13434 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)))) | ||
Theorem | fzrev2i 13435 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀))) | ||
Theorem | fzrev3 13436 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ (𝐾 ∈ ℤ → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁))) | ||
Theorem | fzrev3i 13437 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁)) | ||
Theorem | fznn 13438 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfz1b 13439 | Membership in a 1-based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) (Proof shortened by AV, 23-Jan-2022.) |
⊢ (𝑁 ∈ (1...𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ≤ 𝑀)) | ||
Theorem | elfz1uz 13440 | Membership in a 1-based finite set of sequential integers with an upper integer. (Contributed by AV, 23-Jan-2022.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (1...𝑀)) | ||
Theorem | elfzm11 13441 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) | ||
Theorem | uzsplit 13442 | Express an upper integer set as the disjoint (see uzdisj 13443) union of the first 𝑁 values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑀) = ((𝑀...(𝑁 − 1)) ∪ (ℤ≥‘𝑁))) | ||
Theorem | uzdisj 13443 | The first 𝑁 elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ ((𝑀...(𝑁 − 1)) ∩ (ℤ≥‘𝑁)) = ∅ | ||
Theorem | fseq1p1m1 13444 | Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 7-Mar-2014.) |
⊢ 𝐻 = {⟨(𝑁 + 1), 𝐵⟩} ⇒ ⊢ (𝑁 ∈ ℕ0 → ((𝐹:(1...𝑁)⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻)) ↔ (𝐺:(1...(𝑁 + 1))⟶𝐴 ∧ (𝐺‘(𝑁 + 1)) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...𝑁))))) | ||
Theorem | fseq1m1p1 13445 | Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ 𝐻 = {⟨𝑁, 𝐵⟩} ⇒ ⊢ (𝑁 ∈ ℕ → ((𝐹:(1...(𝑁 − 1))⟶𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = (𝐹 ∪ 𝐻)) ↔ (𝐺:(1...𝑁)⟶𝐴 ∧ (𝐺‘𝑁) = 𝐵 ∧ 𝐹 = (𝐺 ↾ (1...(𝑁 − 1)))))) | ||
Theorem | fz1sbc 13446* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
⊢ (𝑁 ∈ ℤ → (∀𝑘 ∈ (𝑁...𝑁)𝜑 ↔ [𝑁 / 𝑘]𝜑)) | ||
Theorem | elfzp1b 13447 | An integer is a member of a 0-based finite set of sequential integers iff its successor is a member of the corresponding 1-based set. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...(𝑁 − 1)) ↔ (𝐾 + 1) ∈ (1...𝑁))) | ||
Theorem | elfzm1b 13448 | 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 Paul Chapman, 22-Jun-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (1...𝑁) ↔ (𝐾 − 1) ∈ (0...(𝑁 − 1)))) | ||
Theorem | elfzp12 13449 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁)))) | ||
Theorem | fzm1 13450 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) | ||
Theorem | fzneuz 13451 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → ¬ (𝑀...𝑁) = (ℤ≥‘𝐾)) | ||
Theorem | fznuz 13452 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 30-Jun-2013.) (Revised by Mario Carneiro, 24-Aug-2013.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → ¬ 𝐾 ∈ (ℤ≥‘(𝑁 + 1))) | ||
Theorem | uznfz 13453 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
⊢ (𝐾 ∈ (ℤ≥‘𝑁) → ¬ 𝐾 ∈ (𝑀...(𝑁 − 1))) | ||
Theorem | fzp1nel 13454 | One plus the upper bound of a finite set of integers is not a member of that set. (Contributed by Scott Fenton, 16-Dec-2017.) |
⊢ ¬ (𝑁 + 1) ∈ (𝑀...𝑁) | ||
Theorem | fzrevral 13455* | Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))[(𝐾 − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzrevral2 13456* | Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[(𝐾 − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzrevral3 13457* | Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[((𝑀 + 𝑁) − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzshftral 13458* | Shift the scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) | ||
Theorem | ige2m1fz1 13459 | Membership of an integer greater than 1 decreased by 1 in a 1-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → (𝑁 − 1) ∈ (1...𝑁)) | ||
Theorem | ige2m1fz 13460 | Membership in a 0-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 18-Jun-2018.) (Proof shortened by Alexander van der Vekens, 15-Sep-2018.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ (0...𝑁)) | ||
Finite intervals of nonnegative integers (or "finite sets of sequential nonnegative integers") are finite intervals of integers with 0 as lower bound: (0...𝑁), usually abbreviated by "fz0". | ||
Theorem | elfz2nn0 13461 | Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁)) | ||
Theorem | fznn0 13462 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
⊢ (𝑁 ∈ ℕ0 → (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfznn0 13463 | A member of a finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by NM, 5-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ0) | ||
Theorem | elfz3nn0 13464 | The upper bound of a nonempty finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by NM, 16-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ ℕ0) | ||
Theorem | fz0ssnn0 13465 | Finite sets of sequential nonnegative integers starting with 0 are subsets of NN0. (Contributed by JJ, 1-Jun-2021.) |
⊢ (0...𝑁) ⊆ ℕ0 | ||
Theorem | fz1ssfz0 13466 | Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (1...𝑁) ⊆ (0...𝑁) | ||
Theorem | 0elfz 13467 | 0 is an element of a finite set of sequential nonnegative integers with a nonnegative integer as upper bound. (Contributed by AV, 6-Apr-2018.) |
⊢ (𝑁 ∈ ℕ0 → 0 ∈ (0...𝑁)) | ||
Theorem | nn0fz0 13468 | A nonnegative integer is always part of the finite set of sequential nonnegative integers with this integer as upper bound. (Contributed by Scott Fenton, 21-Mar-2018.) |
⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (0...𝑁)) | ||
Theorem | elfz0add 13469 | An element of a finite set of sequential nonnegative integers is an element of an extended finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝑁 ∈ (0...𝐴) → 𝑁 ∈ (0...(𝐴 + 𝐵)))) | ||
Theorem | fz0sn 13470 | An integer range from 0 to 0 is a singleton. (Contributed by AV, 18-Apr-2021.) |
⊢ (0...0) = {0} | ||
Theorem | fz0tp 13471 | An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
⊢ (0...2) = {0, 1, 2} | ||
Theorem | fz0to3un2pr 13472 | An integer range from 0 to 3 is the union of two unordered pairs. (Contributed by AV, 7-Feb-2021.) |
⊢ (0...3) = ({0, 1} ∪ {2, 3}) | ||
Theorem | fz0to4untppr 13473 | An integer range from 0 to 4 is the union of a triple and a pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
⊢ (0...4) = ({0, 1, 2} ∪ {3, 4}) | ||
Theorem | elfz0ubfz0 13474 | 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 13475 | 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 13476 | 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 13477 | 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 13478 | 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 13479 | 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 13480 | 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 13481 | 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 13482 | 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 13483 | 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 13484 | 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 13485 | Express the set of nonnegative integers as the disjoint (see nn0disj 13486) union of the first 𝑁 + 1 values and the rest. (Contributed by AV, 8-Nov-2019.) |
⊢ (𝑁 ∈ ℕ0 → ℕ0 = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) | ||
Theorem | nn0disj 13486 | 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 13487 | 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 13488 | The function value of a function from a finite interval of nonnegative integers. (Contributed by AV, 13-Feb-2021.) |
⊢ (((𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁) ∧ 𝑃:(0...𝑁)⟶𝑉) → (𝑃‘𝐼) ∈ 𝑉) | ||
Theorem | 1fv 13489 | 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 13490* | 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 13491* | 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 13492 | The value of the predecessor class over an upper integer set. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → Pred( < , (ℤ≥‘𝑀), 𝑁) = (𝑀...(𝑁 − 1))) | ||
Theorem | prednn 13493 | The value of the predecessor class over the naturals. (Contributed by Scott Fenton, 6-Aug-2013.) |
⊢ (𝑁 ∈ ℕ → Pred( < , ℕ, 𝑁) = (1...(𝑁 − 1))) | ||
Theorem | prednn0 13494 | The value of the predecessor class over ℕ0. (Contributed by Scott Fenton, 9-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → Pred( < , ℕ0, 𝑁) = (0...(𝑁 − 1))) | ||
Theorem | predfz 13495 | 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 13496 | Syntax for half-open integer ranges. |
class ..^ | ||
Definition | df-fzo 13497* | 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 13354, which includes 𝑁. Not including the endpoint simplifies a number of formulas related to cardinality and splitting; contrast fzosplit 13534 with fzsplit 13396, for instance. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1))) | ||
Theorem | fzof 13498 | Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ | ||
Theorem | elfzoel1 13499 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ) | ||
Theorem | elfzoel2 13500 | Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |