Home | Intuitionistic Logic Explorer Theorem List (p. 95 of 116) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elfz5 9401 | Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.) |
⊢ ((𝐾 ∈ (ℤ_{≥}‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾 ≤ 𝑁)) | ||
Theorem | elfz4 9402 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝐾 ∈ (𝑀...𝑁)) | ||
Theorem | elfzuzb 9403 | Membership in a finite set of sequential integers in terms of sets of upper integers. (Contributed by NM, 18-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ_{≥}‘𝑀) ∧ 𝑁 ∈ (ℤ_{≥}‘𝐾))) | ||
Theorem | eluzfz 9404 | Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐾 ∈ (ℤ_{≥}‘𝑀) ∧ 𝑁 ∈ (ℤ_{≥}‘𝐾)) → 𝐾 ∈ (𝑀...𝑁)) | ||
Theorem | elfzuz 9405 | A member of a finite set of sequential integers belongs to an upper set of integers. (Contributed by NM, 17-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ_{≥}‘𝑀)) | ||
Theorem | elfzuz3 9406 | Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ_{≥}‘𝐾)) | ||
Theorem | elfzel2 9407 | Membership in a finite set of sequential integer implies the upper bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ) | ||
Theorem | elfzel1 9408 | Membership in a finite set of sequential integer implies the lower bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ) | ||
Theorem | elfzelz 9409 | A member of a finite set of sequential integer is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ) | ||
Theorem | elfzle1 9410 | A member of a finite set of sequential integer is greater than or equal to the lower bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾) | ||
Theorem | elfzle2 9411 | A member of a finite set of sequential integer is less than or equal to the upper bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁) | ||
Theorem | elfzuz2 9412 | Implication of membership in a finite set of sequential integers. (Contributed by NM, 20-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ_{≥}‘𝑀)) | ||
Theorem | elfzle3 9413 | Membership in a finite set of sequential integer implies the bounds are comparable. (Contributed by NM, 18-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑁) | ||
Theorem | eluzfz1 9414 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) | ||
Theorem | eluzfz2 9415 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 13-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) | ||
Theorem | eluzfz2b 9416 | Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) ↔ 𝑁 ∈ (𝑀...𝑁)) | ||
Theorem | elfz3 9417 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (𝑁...𝑁)) | ||
Theorem | elfz1eq 9418 | Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005.) |
⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁) | ||
Theorem | elfzubelfz 9419 | If there is a member in a finite set of sequential integers, the upper bound is also a member of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 31-May-2018.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (𝑀...𝑁)) | ||
Theorem | peano2fzr 9420 | A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014.) |
⊢ ((𝐾 ∈ (ℤ_{≥}‘𝑀) ∧ (𝐾 + 1) ∈ (𝑀...𝑁)) → 𝐾 ∈ (𝑀...𝑁)) | ||
Theorem | fzm 9421* | Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.) |
⊢ (∃𝑥 𝑥 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (ℤ_{≥}‘𝑀)) | ||
Theorem | fztri3or 9422 | Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) | ||
Theorem | fzdcel 9423 | Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝐾 ∈ (𝑀...𝑁)) | ||
Theorem | fznlem 9424 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 → (𝑀...𝑁) = ∅)) | ||
Theorem | fzn 9425 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅)) | ||
Theorem | fzen 9426 | A shifted finite set of sequential integers is equinumerous to the original set. (Contributed by Paul Chapman, 11-Apr-2009.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) | ||
Theorem | fz1n 9427 | A 1-based finite set of sequential integers is empty iff it ends at index 0. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝑁 ∈ ℕ_{0} → ((1...𝑁) = ∅ ↔ 𝑁 = 0)) | ||
Theorem | 0fz1 9428 | Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012.) |
⊢ ((𝑁 ∈ ℕ_{0} ∧ 𝐹 Fn (1...𝑁)) → (𝐹 = ∅ ↔ 𝑁 = 0)) | ||
Theorem | fz10 9429 | There are no integers between 1 and 0. (Contributed by Jeff Madsen, 16-Jun-2010.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
⊢ (1...0) = ∅ | ||
Theorem | uzsubsubfz 9430 | Membership of an integer greater than L decreased by ( L - M ) in an M based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.) |
⊢ ((𝐿 ∈ (ℤ_{≥}‘𝑀) ∧ 𝑁 ∈ (ℤ_{≥}‘𝐿)) → (𝑁 − (𝐿 − 𝑀)) ∈ (𝑀...𝑁)) | ||
Theorem | uzsubsubfz1 9431 | Membership of an integer greater than L decreased by ( L - 1 ) in a 1 based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.) |
⊢ ((𝐿 ∈ ℕ ∧ 𝑁 ∈ (ℤ_{≥}‘𝐿)) → (𝑁 − (𝐿 − 1)) ∈ (1...𝑁)) | ||
Theorem | ige3m2fz 9432 | Membership of an integer greater than 2 decreased by 2 in a 1 based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘3) → (𝑁 − 2) ∈ (1...𝑁)) | ||
Theorem | fzsplit2 9433 | Split a finite interval of integers into two parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
⊢ (((𝐾 + 1) ∈ (ℤ_{≥}‘𝑀) ∧ 𝑁 ∈ (ℤ_{≥}‘𝐾)) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁))) | ||
Theorem | fzsplit 9434 | Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 13-Apr-2016.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑀...𝑁) = ((𝑀...𝐾) ∪ ((𝐾 + 1)...𝑁))) | ||
Theorem | fzdisj 9435 | Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.) |
⊢ (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅) | ||
Theorem | fz01en 9436 | 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009.) |
⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁)) | ||
Theorem | elfznn 9437 | A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005.) |
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ) | ||
Theorem | elfz1end 9438 | A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴)) | ||
Theorem | fznn0sub 9439 | 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 9440 | 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 9441 | Membership of a sum in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) | ||
Theorem | fzsubel 9442 | Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐽 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝑀 − 𝐾)...(𝑁 − 𝐾)))) | ||
Theorem | fzopth 9443 | A finite set of sequential integers can represent an ordered pair. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾))) | ||
Theorem | fzass4 9444 | Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐵 ∈ (𝐴...𝐷) ∧ 𝐶 ∈ (𝐵...𝐷)) ↔ (𝐵 ∈ (𝐴...𝐶) ∧ 𝐶 ∈ (𝐴...𝐷))) | ||
Theorem | fzss1 9445 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐾 ∈ (ℤ_{≥}‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) | ||
Theorem | fzss2 9446 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁)) | ||
Theorem | fzssuz 9447 | A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
⊢ (𝑀...𝑁) ⊆ (ℤ_{≥}‘𝑀) | ||
Theorem | fzsn 9448 | A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) | ||
Theorem | fzssp1 9449 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1)) | ||
Theorem | fzsuc 9450 | 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 9451 | Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) | ||
Theorem | fzpreddisj 9452 | A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → ({𝑀} ∩ ((𝑀 + 1)...𝑁)) = ∅) | ||
Theorem | elfzp1 9453 | 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 9454 | Subset relationship for finite sets of sequential integers. (Contributed by NM, 26-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) | ||
Theorem | fzelp1 9455 | 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 9456 | 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 9457 | Shift membership in a finite sequence of naturals. (Contributed by Scott Fenton, 17-Jul-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (𝐼 + 1) ∈ (1...𝑁)) | ||
Theorem | fzpr 9458 | A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)}) | ||
Theorem | fztp 9459 | 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 | fzsuc2 9460 | 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 9461 | (𝑀...(𝑁 + 1)) is the disjoint union of (𝑀...𝑁) with {(𝑁 + 1)}. (Contributed by Mario Carneiro, 7-Mar-2014.) |
⊢ ((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅ | ||
Theorem | fzdifsuc 9462 | Remove a successor from the end of a finite set of sequential integers. (Contributed by AV, 4-Sep-2019.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) | ||
Theorem | fzprval 9463* | 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 9464* | 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 9465 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)) ↔ (𝐽 − 𝐾) ∈ (𝑀...𝑁))) | ||
Theorem | fzrev2 9466 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀)))) | ||
Theorem | fzrev2i 9467 | Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝐽 ∈ ℤ ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐽 − 𝐾) ∈ ((𝐽 − 𝑁)...(𝐽 − 𝑀))) | ||
Theorem | fzrev3 9468 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ (𝐾 ∈ ℤ → (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁))) | ||
Theorem | fzrev3i 9469 | The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ (𝐾 ∈ (𝑀...𝑁) → ((𝑀 + 𝑁) − 𝐾) ∈ (𝑀...𝑁)) | ||
Theorem | fznn 9470 | Finite set of sequential integers starting at 1. (Contributed by NM, 31-Aug-2011.) (Revised by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfz1b 9471 | Membership in a 1 based finite set of sequential integers. (Contributed by AV, 30-Oct-2018.) |
⊢ (𝑁 ∈ (1...𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ≤ 𝑀)) | ||
Theorem | elfzm11 9472 | Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) | ||
Theorem | uzsplit 9473 | Express an upper integer set as the disjoint (see uzdisj 9474) union of the first 𝑁 values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (ℤ_{≥}‘𝑀) = ((𝑀...(𝑁 − 1)) ∪ (ℤ_{≥}‘𝑁))) | ||
Theorem | uzdisj 9474 | The first 𝑁 elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014.) |
⊢ ((𝑀...(𝑁 − 1)) ∩ (ℤ_{≥}‘𝑁)) = ∅ | ||
Theorem | fseq1p1m1 9475 | 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 9476 | 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 9477* | Quantification over a one-member finite set of sequential integers in terms of substitution. (Contributed by NM, 28-Nov-2005.) |
⊢ (𝑁 ∈ ℤ → (∀𝑘 ∈ (𝑁...𝑁)𝜑 ↔ [𝑁 / 𝑘]𝜑)) | ||
Theorem | elfzp1b 9478 | 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 9479 | 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 9480 | Options for membership in a finite interval of integers. (Contributed by Jeff Madsen, 18-Jun-2010.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)...𝑁)))) | ||
Theorem | fzm1 9481 | Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) | ||
Theorem | fzneuz 9482 | No finite set of sequential integers equals an upper set of integers. (Contributed by NM, 11-Dec-2005.) |
⊢ ((𝑁 ∈ (ℤ_{≥}‘𝑀) ∧ 𝐾 ∈ ℤ) → ¬ (𝑀...𝑁) = (ℤ_{≥}‘𝐾)) | ||
Theorem | fznuz 9483 | 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 9484 | Disjointness of the upper integers and a finite sequence. (Contributed by Mario Carneiro, 24-Aug-2013.) |
⊢ (𝐾 ∈ (ℤ_{≥}‘𝑁) → ¬ 𝐾 ∈ (𝑀...(𝑁 − 1))) | ||
Theorem | fzp1nel 9485 | 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 9486* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))[(𝐾 − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzrevral2 9487* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 25-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ ((𝐾 − 𝑁)...(𝐾 − 𝑀))𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[(𝐾 − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzrevral3 9488* | Reversal of scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 20-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ (𝑀...𝑁)[((𝑀 + 𝑁) − 𝑘) / 𝑗]𝜑)) | ||
Theorem | fzshftral 9489* | Shift the scanning order inside of a quantification over a finite set of sequential integers. (Contributed by NM, 27-Nov-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀...𝑁)𝜑 ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]𝜑)) | ||
Theorem | ige2m1fz1 9490 | 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 9491 | 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...𝑁)) | ||
Theorem | fz01or 9492 | An integer is in the integer range from zero to one iff it is either zero or one. (Contributed by Jim Kingdon, 11-Nov-2021.) |
⊢ (𝐴 ∈ (0...1) ↔ (𝐴 = 0 ∨ 𝐴 = 1)) | ||
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 9493 | 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 9494 | Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005.) |
⊢ (𝑁 ∈ ℕ_{0} → (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ_{0} ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | elfznn0 9495 | 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 9496 | 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 | 0elfz 9497 | 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 9498 | 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 9499 | 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 | fz0tp 9500 | 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} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |