![]() |
Intuitionistic Logic Explorer Theorem List (p. 89 of 95) | < 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 | fzossnn0 8801 | 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 8802 | One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ((A ∈ (B..^𝐶) ∧ 𝐷 ∈ ℤ) → (A ∈ (B..^𝐷) ∨ A ∈ (𝐷..^𝐶))) | ||
Theorem | fzosplit 8803 | Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐷 ∈ (B...𝐶) → (B..^𝐶) = ((B..^𝐷) ∪ (𝐷..^𝐶))) | ||
Theorem | fzodisj 8804 | Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ ((A..^B) ∩ (B..^𝐶)) = ∅ | ||
Theorem | fzouzsplit 8805 | Split an upper integer set into a half-open integer range and another upper integer set. (Contributed by Mario Carneiro, 21-Sep-2016.) |
⊢ (B ∈ (ℤ≥‘A) → (ℤ≥‘A) = ((A..^B) ∪ (ℤ≥‘B))) | ||
Theorem | fzouzdisj 8806 | 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.) |
⊢ ((A..^B) ∩ (ℤ≥‘B)) = ∅ | ||
Theorem | lbfzo0 8807 | An integer is strictly greater than zero iff it is a member of ℕ. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (0 ∈ (0..^A) ↔ A ∈ ℕ) | ||
Theorem | elfzo0 8808 | 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.) |
⊢ (A ∈ (0..^B) ↔ (A ∈ ℕ0 ∧ B ∈ ℕ ∧ A < B)) | ||
Theorem | fzo1fzo0n0 8809 | 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 | elfzo0z 8810 | Membership in a half-open range of nonnegative integers, generalization of elfzo0 8808 requiring the upper bound to be an integer only. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ (A ∈ (0..^B) ↔ (A ∈ ℕ0 ∧ B ∈ ℤ ∧ A < B)) | ||
Theorem | elfzo0le 8811 | 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.) |
⊢ (A ∈ (0..^B) → A ≤ B) | ||
Theorem | elfzonn0 8812 | 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 8813 | 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.) |
⊢ ((A ∈ (0..^𝑁) ∧ B ∈ (0..^𝑁) ∧ B < A) → (B + (𝑁 − A)) < 𝑁) | ||
Theorem | fzofzim 8814 | 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 | fzossnn 8815 | Half-open integer ranges starting with 1 are subsets of NN. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
⊢ (1..^𝑁) ⊆ ℕ | ||
Theorem | elfzo1 8816 | Membership in a half-open integer range based at 1. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝑁 ∈ (1..^𝑀) ↔ (𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 < 𝑀)) | ||
Theorem | fzo0m 8817* | 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.) |
⊢ (∃x x ∈ (0..^A) ↔ A ∈ ℕ) | ||
Theorem | fzoaddel 8818 | Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((A ∈ (B..^𝐶) ∧ 𝐷 ∈ ℤ) → (A + 𝐷) ∈ ((B + 𝐷)..^(𝐶 + 𝐷))) | ||
Theorem | fzoaddel2 8819 | Translate membership in a shifted-down half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((A ∈ (0..^(B − 𝐶)) ∧ B ∈ ℤ ∧ 𝐶 ∈ ℤ) → (A + 𝐶) ∈ (𝐶..^B)) | ||
Theorem | fzosubel 8820 | Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((A ∈ (B..^𝐶) ∧ 𝐷 ∈ ℤ) → (A − 𝐷) ∈ ((B − 𝐷)..^(𝐶 − 𝐷))) | ||
Theorem | fzosubel2 8821 | Membership in a translated half-open integer range implies translated membership in the original range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((A ∈ ((B + 𝐶)..^(B + 𝐷)) ∧ (B ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (A − B) ∈ (𝐶..^𝐷)) | ||
Theorem | fzosubel3 8822 | Membership in a translated half-open integer range when the original range is zero-based. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((A ∈ (B..^(B + 𝐷)) ∧ 𝐷 ∈ ℤ) → (A − B) ∈ (0..^𝐷)) | ||
Theorem | eluzgtdifelfzo 8823 | Membership of the difference of integers in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → ((𝑁 ∈ (ℤ≥‘A) ∧ B < A) → (𝑁 − A) ∈ (0..^(𝑁 − B)))) | ||
Theorem | ige2m2fzo 8824 | 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 8825 | Translate membership in a half-open integer range. (Contributed by Thierry Arnoux, 28-Sep-2018.) |
⊢ (((A ∈ (0..^(B + 𝐶)) ∧ ¬ A ∈ (0..^B)) ∧ (B ∈ ℤ ∧ 𝐶 ∈ ℤ)) → (A − B) ∈ (0..^𝐶)) | ||
Theorem | ubmelfzo 8826 | 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 8827 | 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 8828 | 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 8829 | Membership in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 18-Jun-2018.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(𝑁 − 1))) → 𝐼 ∈ (0..^𝑁)) | ||
Theorem | fzval3 8830 | Expressing a closed integer range as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝑁 ∈ ℤ → (𝑀...𝑁) = (𝑀..^(𝑁 + 1))) | ||
Theorem | fzosn 8831 | Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (A ∈ ℤ → (A..^(A + 1)) = {A}) | ||
Theorem | elfzomin 8832 | Membership of an integer in the smallest open range of integers. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ (𝑍 ∈ ℤ → 𝑍 ∈ (𝑍..^(𝑍 + 1))) | ||
Theorem | zpnn0elfzo 8833 | 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 8834 | 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 8835 | Removing a singleton from a half-open integer range at the end. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
⊢ ((A ∈ ℤ ∧ B ∈ (ℤ≥‘(A + 1))) → (A..^B) = ((A..^(B − 1)) ∪ {(B − 1)})) | ||
Theorem | elfzonlteqm1 8836 | 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.) |
⊢ ((A ∈ (0..^B) ∧ ¬ A < (B − 1)) → A = (B − 1)) | ||
Theorem | fzonn0p1 8837 | 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 8838 | 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 8839 | 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 8840 | 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.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ (0..^(𝑁 − 1))) → (𝑋 + 1) ∈ (0..^𝑁)) | ||
Theorem | fzo0ssnn0 8841 | Half-open integer ranges starting with 0 are subsets of NN0. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
⊢ (0..^𝑁) ⊆ ℕ0 | ||
Theorem | fzo01 8842 | Expressing the singleton of 0 as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (0..^1) = {0} | ||
Theorem | fzo12sn 8843 | 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 | fzo0to2pr 8844 | 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 | fzo0to3tp 8845 | 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 8846 | 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 | fzo0sn0fzo1 8847 | 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 | fzoend 8848 | The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ (A ∈ (A..^B) → (B − 1) ∈ (A..^B)) | ||
Theorem | fzo0end 8849 | The endpoint of a zero-based half-open range. (Contributed by Stefan O'Rear, 27-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.) |
⊢ (B ∈ ℕ → (B − 1) ∈ (0..^B)) | ||
Theorem | ssfzo12 8850 | Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | ||
Theorem | ssfzo12bi 8851 | Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 5-Nov-2018.) |
⊢ (((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝐿) → ((𝐾..^𝐿) ⊆ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | ||
Theorem | ubmelm1fzo 8852 | 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.) |
⊢ (𝐾 ∈ (0..^𝑁) → ((𝑁 − 𝐾) − 1) ∈ (0..^𝑁)) | ||
Theorem | fzofzp1 8853 | 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.) |
⊢ (𝐶 ∈ (A..^B) → (𝐶 + 1) ∈ (A...B)) | ||
Theorem | fzofzp1b 8854 | If a point is in a half-open range, the next point is in the closed range. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (𝐶 ∈ (ℤ≥‘A) → (𝐶 ∈ (A..^B) ↔ (𝐶 + 1) ∈ (A...B))) | ||
Theorem | elfzom1b 8855 | 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.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (1..^𝑁) ↔ (𝐾 − 1) ∈ (0..^(𝑁 − 1)))) | ||
Theorem | elfzonelfzo 8856 | 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 8857 | 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 8858 | A Peano-postulate-like theorem for downward closure of a half-open integer range. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ ((𝐾 ∈ (ℤ≥‘𝑀) ∧ (𝐾 + 1) ∈ (𝑀..^𝑁)) → 𝐾 ∈ (𝑀..^𝑁)) | ||
Theorem | fzosplitsn 8859 | Extending a half-open range by a singleton on the end. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (B ∈ (ℤ≥‘A) → (A..^(B + 1)) = ((A..^B) ∪ {B})) | ||
Theorem | fzosplitprm1 8860 | Extending a half-open integer range by an unordered pair at the end. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((A ∈ ℤ ∧ B ∈ ℤ ∧ A < B) → (A..^(B + 1)) = ((A..^(B − 1)) ∪ {(B − 1), B})) | ||
Theorem | fzosplitsni 8861 | Membership in a half-open range extended by a singleton. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (B ∈ (ℤ≥‘A) → (𝐶 ∈ (A..^(B + 1)) ↔ (𝐶 ∈ (A..^B) ∨ 𝐶 = B))) | ||
Theorem | fzisfzounsn 8862 | 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.) |
⊢ (B ∈ (ℤ≥‘A) → (A...B) = ((A..^B) ∪ {B})) | ||
Theorem | fzostep1 8863 | Two possibilities for a number one greater than a number in a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ (A ∈ (B..^𝐶) → ((A + 1) ∈ (B..^𝐶) ∨ (A + 1) = 𝐶)) | ||
Theorem | fzoshftral 8864* | Shift the scanning order inside of a quantification over a half-open integer range, analogous to fzshftral 8740. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (∀𝑗 ∈ (𝑀..^𝑁)φ ↔ ∀𝑘 ∈ ((𝑀 + 𝐾)..^(𝑁 + 𝐾))[(𝑘 − 𝐾) / 𝑗]φ)) | ||
Theorem | fzind2 8865* | 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 8129 using integer range definitions. (Contributed by Mario Carneiro, 6-Feb-2016.) |
⊢ (x = 𝑀 → (φ ↔ ψ)) & ⊢ (x = y → (φ ↔ χ)) & ⊢ (x = (y + 1) → (φ ↔ θ)) & ⊢ (x = 𝐾 → (φ ↔ τ)) & ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ψ) & ⊢ (y ∈ (𝑀..^𝑁) → (χ → θ)) ⇒ ⊢ (𝐾 ∈ (𝑀...𝑁) → τ) | ||
Theorem | frec2uz0d 8866* | The mapping 𝐺 is a one-to-one mapping from 𝜔 onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number 𝐶 (normally 0 for the upper integers ℕ0 or 1 for the upper integers ℕ), 1 maps to 𝐶 + 1, etc. This theorem shows the value of 𝐺 at ordinal natural number zero. (Contributed by Jim Kingdon, 16-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) ⇒ ⊢ (φ → (𝐺‘∅) = 𝐶) | ||
Theorem | frec2uzzd 8867* | The value of 𝐺 (see frec2uz0d 8866) is an integer. (Contributed by Jim Kingdon, 16-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → A ∈ 𝜔) ⇒ ⊢ (φ → (𝐺‘A) ∈ ℤ) | ||
Theorem | frec2uzsucd 8868* | The value of 𝐺 (see frec2uz0d 8866) at a successor. (Contributed by Jim Kingdon, 16-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → A ∈ 𝜔) ⇒ ⊢ (φ → (𝐺‘suc A) = ((𝐺‘A) + 1)) | ||
Theorem | frec2uzuzd 8869* | The value 𝐺 (see frec2uz0d 8866) at an ordinal natural number is in the upper integers. (Contributed by Jim Kingdon, 16-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → A ∈ 𝜔) ⇒ ⊢ (φ → (𝐺‘A) ∈ (ℤ≥‘𝐶)) | ||
Theorem | frec2uzltd 8870* | Less-than relation for 𝐺 (see frec2uz0d 8866). (Contributed by Jim Kingdon, 16-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → A ∈ 𝜔) & ⊢ (φ → B ∈ 𝜔) ⇒ ⊢ (φ → (A ∈ B → (𝐺‘A) < (𝐺‘B))) | ||
Theorem | frec2uzlt2d 8871* | The mapping 𝐺 (see frec2uz0d 8866) preserves order. (Contributed by Jim Kingdon, 16-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → A ∈ 𝜔) & ⊢ (φ → B ∈ 𝜔) ⇒ ⊢ (φ → (A ∈ B ↔ (𝐺‘A) < (𝐺‘B))) | ||
Theorem | frec2uzrand 8872* | Range of 𝐺 (see frec2uz0d 8866). (Contributed by Jim Kingdon, 17-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) ⇒ ⊢ (φ → ran 𝐺 = (ℤ≥‘𝐶)) | ||
Theorem | frec2uzf1od 8873* | 𝐺 (see frec2uz0d 8866) is a one-to-one onto mapping. (Contributed by Jim Kingdon, 17-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) ⇒ ⊢ (φ → 𝐺:𝜔–1-1-onto→(ℤ≥‘𝐶)) | ||
Theorem | frec2uzisod 8874* | 𝐺 (see frec2uz0d 8866) is an isomorphism from natural ordinals to upper integers. (Contributed by Jim Kingdon, 17-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) ⇒ ⊢ (φ → 𝐺 Isom E , < (𝜔, (ℤ≥‘𝐶))) | ||
Theorem | frecuzrdgrrn 8875* | The function 𝑅 (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of 𝑆. (Contributed by Jim Kingdon, 27-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ 〈(x + 1), (x𝐹y)〉), 〈𝐶, A〉) ⇒ ⊢ ((φ ∧ 𝐷 ∈ 𝜔) → (𝑅‘𝐷) ∈ ((ℤ≥‘𝐶) × 𝑆)) | ||
Theorem | frec2uzrdg 8876* | A helper lemma for the value of a recursive definition generator on upper integers (typically either ℕ or ℕ0) with characteristic function 𝐹(x, y) and initial value A. This lemma shows that evaluating 𝑅 at an element of 𝜔 gives an ordered pair whose first element is the index (translated from 𝜔 to (ℤ≥‘𝐶)). See comment in frec2uz0d 8866 which describes 𝐺 and the index translation. (Contributed by Jim Kingdon, 24-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ 〈(x + 1), (x𝐹y)〉), 〈𝐶, A〉) & ⊢ (φ → B ∈ 𝜔) ⇒ ⊢ (φ → (𝑅‘B) = 〈(𝐺‘B), (2nd ‘(𝑅‘B))〉) | ||
Theorem | frecuzrdgrom 8877* | The function 𝑅 (used in the definition of the recursive definition generator on upper integers) is a function defined for all natural numbers. (Contributed by Jim Kingdon, 26-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ 〈(x + 1), (x𝐹y)〉), 〈𝐶, A〉) ⇒ ⊢ (φ → 𝑅 Fn 𝜔) | ||
Theorem | frecuzrdglem 8878* | A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 26-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ 〈(x + 1), (x𝐹y)〉), 〈𝐶, A〉) & ⊢ (φ → B ∈ (ℤ≥‘𝐶)) ⇒ ⊢ (φ → 〈B, (2nd ‘(𝑅‘(◡𝐺‘B)))〉 ∈ ran 𝑅) | ||
Theorem | frecuzrdgfn 8879* | The recursive definition generator on upper integers is a function. See comment in frec2uz0d 8866 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 26-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ 〈(x + 1), (x𝐹y)〉), 〈𝐶, A〉) & ⊢ (φ → 𝑇 = ran 𝑅) ⇒ ⊢ (φ → 𝑇 Fn (ℤ≥‘𝐶)) | ||
Theorem | frecuzrdgcl 8880* | Closure law for the recursive definition generator on upper integers. See comment in frec2uz0d 8866 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 31-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ 〈(x + 1), (x𝐹y)〉), 〈𝐶, A〉) & ⊢ (φ → 𝑇 = ran 𝑅) ⇒ ⊢ ((φ ∧ B ∈ (ℤ≥‘𝐶)) → (𝑇‘B) ∈ 𝑆) | ||
Theorem | frecuzrdg0 8881* | Initial value of a recursive definition generator on upper integers. See comment in frec2uz0d 8866 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 27-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ 〈(x + 1), (x𝐹y)〉), 〈𝐶, A〉) & ⊢ (φ → 𝑇 = ran 𝑅) ⇒ ⊢ (φ → (𝑇‘𝐶) = A) | ||
Theorem | frecuzrdgsuc 8882* | Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 8866 for the description of 𝐺 as the mapping from 𝜔 to (ℤ≥‘𝐶). (Contributed by Jim Kingdon, 28-May-2020.) |
⊢ (φ → 𝐶 ∈ ℤ) & ⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 𝐶) & ⊢ (φ → 𝑆 ∈ 𝑉) & ⊢ (φ → A ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝐶) ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) & ⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝐶), y ∈ 𝑆 ↦ 〈(x + 1), (x𝐹y)〉), 〈𝐶, A〉) & ⊢ (φ → 𝑇 = ran 𝑅) ⇒ ⊢ ((φ ∧ B ∈ (ℤ≥‘𝐶)) → (𝑇‘(B + 1)) = (B𝐹(𝑇‘B))) | ||
Theorem | uzenom 8883 | An upper integer set is denumerable. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → 𝑍 ≈ 𝜔) | ||
Theorem | frecfzennn 8884 | The cardinality of a finite set of sequential integers. (See frec2uz0d 8866 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.) |
⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 0) ⇒ ⊢ (𝑁 ∈ ℕ0 → (1...𝑁) ≈ (◡𝐺‘𝑁)) | ||
Theorem | frecfzen2 8885 | The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Jim Kingdon, 18-May-2020.) |
⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 0) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡𝐺‘((𝑁 + 1) − 𝑀))) | ||
Theorem | frechashgf1o 8886 | 𝐺 maps 𝜔 one-to-one onto ℕ0. (Contributed by Jim Kingdon, 19-May-2020.) |
⊢ 𝐺 = frec((x ∈ ℤ ↦ (x + 1)), 0) ⇒ ⊢ 𝐺:𝜔–1-1-onto→ℕ0 | ||
Theorem | fzfig 8887 | A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) ∈ Fin) | ||
Theorem | fzfigd 8888 | Deduction form of fzfig 8887. (Contributed by Jim Kingdon, 21-May-2020.) |
⊢ (φ → 𝑀 ∈ ℤ) & ⊢ (φ → 𝑁 ∈ ℤ) ⇒ ⊢ (φ → (𝑀...𝑁) ∈ Fin) | ||
Theorem | fzofig 8889 | Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) ∈ Fin) | ||
Theorem | nn0ennn 8890 | The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004.) |
⊢ ℕ0 ≈ ℕ | ||
Theorem | nnenom 8891 | The set of positive integers (as a subset of complex numbers) is equinumerous to omega (the set of finite ordinal numbers). (Contributed by NM, 31-Jul-2004.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ ℕ ≈ 𝜔 | ||
Syntax | cseq 8892 | Extend class notation with recursive sequence builder. |
class seq𝑀( + , 𝐹, 𝑆) | ||
Definition | df-iseq 8893* |
Define a general-purpose operation that builds a recursive sequence
(i.e. a function on the positive integers ℕ or some other upper
integer set) whose value at an index is a function of its previous value
and the value of an input sequence at that index. This definition is
complicated, but fortunately it is not intended to be used directly.
Instead, the only purpose of this definition is to provide us with an
object that has the properties expressed by iseq1 8902 and iseqp1 8904.
Typically, those are the main theorems that would be used in practice.
The first operand in the parentheses is the operation that is applied to the previous value and the value of the input sequence (second operand). The operand to the left of the parenthesis is the integer to start from. For example, for the operation +, an input sequence 𝐹 with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence seq1( + , 𝐹, ℚ) with values 1, 3/2, 7/4, 15/8,.., so that (seq1( + , 𝐹, ℚ)‘1) = 1, (seq1( + , 𝐹, ℚ)‘2) = 3/2, etc. In other words, seq𝑀( + , 𝐹, ℚ) transforms a sequence 𝐹 into an infinite series. Internally, the frec function generates as its values a set of ordered pairs starting at 〈𝑀, (𝐹‘𝑀)〉, with the first member of each pair incremented by one in each successive value. So, the range of frec is exactly the sequence we want, and we just extract the range and throw away the domain. (Contributed by Jim Kingdon, 29-May-2020.) |
⊢ seq𝑀( + , 𝐹, 𝑆) = ran frec((x ∈ (ℤ≥‘𝑀), y ∈ 𝑆 ↦ 〈(x + 1), (y + (𝐹‘(x + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) | ||
Theorem | iseqeq1 8894 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹, 𝑆) = seq𝑁( + , 𝐹, 𝑆)) | ||
Theorem | iseqeq2 8895 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ ( + = 𝑄 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀(𝑄, 𝐹, 𝑆)) | ||
Theorem | iseqeq3 8896 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐺, 𝑆)) | ||
Theorem | iseqeq4 8897 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ (𝑆 = 𝑇 → seq𝑀( + , 𝐹, 𝑆) = seq𝑀( + , 𝐹, 𝑇)) | ||
Theorem | nfiseq 8898 | Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ Ⅎx𝑀 & ⊢ Ⅎx + & ⊢ Ⅎx𝐹 & ⊢ Ⅎx𝑆 ⇒ ⊢ Ⅎxseq𝑀( + , 𝐹, 𝑆) | ||
Theorem | iseqovex 8899* | Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.) |
⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ ((φ ∧ (x ∈ (ℤ≥‘𝑀) ∧ y ∈ 𝑆)) → (x(z ∈ (ℤ≥‘𝑀), w ∈ 𝑆 ↦ (w + (𝐹‘(z + 1))))y) ∈ 𝑆) | ||
Theorem | iseqval 8900* | Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ 𝑅 = frec((x ∈ (ℤ≥‘𝑀), y ∈ 𝑆 ↦ 〈(x + 1), (x(z ∈ (ℤ≥‘𝑀), w ∈ 𝑆 ↦ (w + (𝐹‘(z + 1))))y)〉), 〈𝑀, (𝐹‘𝑀)〉) & ⊢ ((φ ∧ x ∈ (ℤ≥‘𝑀)) → (𝐹‘x) ∈ 𝑆) & ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆) ⇒ ⊢ (φ → seq𝑀( + , 𝐹, 𝑆) = ran 𝑅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |